AVACS

The project addresses the rigorous mathematical verification and analysis of models and realizations 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 a 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 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.
• Such models must cover all typical system structures in this application domain. These include models of distributed target architectures (such as hierarchical bus-structures connecting multiple electronic control units), task models (depicting hierarchical task structures with communication and timing requirements), specification models of electronic control units (such as a controller enforcing a speed-profile), system models (e.g., of the electronic on-board train systems), and models of systems-of-systems (e.g., for coordination of train movements).
• We will address 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.

Today’s v&a technology (see Phase 1 proposal, Section 1.1.2, as well as up-dates to the state of art in subproject proposals) addresses limited subclasses 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 or robust satisfaction relations), the combination of the individual, complementing automated verification techniques will deliver synergies that we do not see in present verification systems.