AVACS – Automatic Verification and Analysis of Complex Systems
This project addresses the rigorous mathematical analysis of models of complex safety critical computerized systems, such as aircrafts, trains, cars, or other artifacts, whose failure can endanger human life. Our aim is to raise the state of the art in automatic verification and analysis techniques (v&a) from its current level, where it is applicable only to isolated facets (concurrency, time, continuous control, stability, dependability, mobility, data structures, hardware constraints, modularity, levels of refinement), to a level allowing a comprehensive and holistic verification of such systems.
We will investigate the mathematical models and their interrelationship as they arise at the various levels of design of safety critical computerized systems. These models range from classical non-deterministic transition systems to probabilistic, real-time, and hybrid system models.
We will, in particular, deal with the complete range of time-models needed to support the development of concrete systems, and the transition between them. This includes the determination of safe sampling rates in plant control as well as the transition between virtual time models and physical execution time.
We will also address a wide range of system structures in this application domain. These range from models of distributed target architectures (such as hierarchical bus-structures connecting multiple electronic control units) to task models (depicting hierarchical task structures with communication and timing requirements) to specification models of electronic control units (such as a controller enforcing a speed-profile) to system models (e.g. of the electronic on-board train systems) to inter-system specification models (e.g. for coordination of train movements).
Today’s v&a technology at best addresses isolated points in this space of models. The proposed project sets out to develop automatic verification techniques covering the entire space. It is our firm belief that by improving and better automating base verification methods (such as abstract interpretation, SAT solvers, symbolic model checking, abstraction techniques, linear programming, constraint solving, Lyapunov functions, automatic decision procedures for relevant first-order theories, automata based verification, heuristic search) and by integrating them in a deep and focused manner we will be able to achieve a dramatic increase in the complexity of models amenable to automatic verification. (By complexity we mean both system size as well as logical complexity as induced by the interferences between the various facets of the system.) By identifying new, as well as by exploiting well-established design and modeling paradigms (mathematically reflected by decomposition theorems that break down complex systems into manageable sub-systems and facets), the combination of the individual, complementing automated verification techniques will deliver synergies that we do not see in present verification systems.