# Projects

## Parametric verification of time critical autonomous systems

Wojciech Penczek (Institute of Computer Science) penczek >at> ipipan.waw.pl

**Description:**Automated verification of finite-state real-time systems, performed by analysis of their models (model checking Clarke et al., 1999), is a very important subject of research. This is highly motivated by an increasing demand to verify safety critical systems, i.e., time-dependent autonomous systems, failure of which could cause dramatic consequences for both people and hardware. These systems include fire alarms, radiation therapy and robotic surgery machines, nuclear reactor control systems, railway signaling, braking systems, air traffic control and flight planning systems, and rocket range launch safety systems etc. Verification of safety critical systems is known to be a difficult problem. Verifying a correctness property of a system amounts to checking whether a logical formula (expressing the property) is valid on a model of the system representing all its possible computations. However, the practical applicability of model checking is strongly limited by the state explosion problem, which means that the number of model states grows exponentially in the size of the system. Parametric Model Checking (PMC) consists in finding the values of the parameters of a model M and/or a formula F, for which F holds in M; allowing this way for finding parameters making models correct. This is a more important and more complicated problem than the standard model checking. However, the high complexity of PMC is the main reason limiting its practical applications. It turns out that satisfiability in the Presburger Arithmetic (PA) is a subproblem of parametric model checking of Timed Computation Tree Logic (TCTL). In case of the translation of the existential fragment of TCTL to PA formulae (Bruyere et al., 2008), the complexity of PMC is 3EXPTIME. Moreover, PMC for unrestricted Parametric Timed Automata (Alur et al., 1993) is undecidable. This causes that the proposed algorithms need not to stop (Hune et al., 2001)

Bounded Model Checking (BMC) is a method of performing verification by stepwise unwinding a verified model and translating the resulting fragment, as well as the property in question, to a propositional formula. The resulting formula is then checked by means of efficient external tools, i.e., SAT-solvers. Alternatively, BMC can be based on a translation to Binary Decision Diagrams (BDDs). This method is usually incomplete from the practical point of view, but it can find counter-examples in systems that appear too large for other approaches. We believe that applying bounded approach to PMC [40, 46] will, in many cases, make parametric verification feasible and more efficient. Our objectives in the project include the following four tasks.

- Task 1
- takes aim at investigating how to apply BMC to parametrized temporal/epistemic logics and parametric timed models.
- Task 2
- is the derivation of effective abstraction techniques for the logics of T1. This is an area where considerable progress can be made towards alleviating the large state spaces of systems.
- Task 3
- is to devise parallel parametric model checking algorithms with little communication overhead, based on these available for model checking modal mi-calculus (Grumberg et al., 2005).
- Task 4
- is to implement the methods developed in Task 1-Task 3 into a new module of the toolkit VerICS (Kacprzak et al., 2008) of ICS PAS.