The AVACS project addresses the rigorous mathematical verification and analysis of models and realizations of complex safety-critical computerized systems, such as aircraft, trains, cars, or networks formed by these, 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 of the underlying space of mathematical models, 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 designing safety-critical computerized systems. Behavioral models range from classical nondeterministic transition systems to probabilistic, real-time, and hybrid system models, to models reflecting the dynamic evolution of the system’s communication structure.

• The investigated classes of models cover all typical system structures in the transportation domain, describing how to build models of complex systems hierarchically from such classes of models. These include distributed target architectures (such as hierarchical bus structures connecting multiple electronic control units), task models (task structures coming with communication and timing requirements), specification models of electronic control units (such as captured in Matlab/Simulink), system models (e.g., of vehicles), and models of systems of systems (e.g., for coordinated vehicle maneuvers).

• The investigated classes of time models are expressive enough to cover all layers of the design space of such applications, including physical latencies of vehicles in performing coordinated maneuvers, system-level timing requirements such as response times to external events and timeliness requirements for protocols, dense-time closed-loop models of controllers and plants, discrete-time design models of controllers, end-to-end deadlines on task chains, and worst-case execution times of tasks on modern processor architectures.

• We provide largely automatic techniques to verify or falsify the compliance of models expressed in this rich model space against classes of requirements subsuming timeliness, safety, probabilistic reachability, stability and other classes of requirements, formalized in suitable logics.

• We provide methods and tools for building such formal proofs for complete systems from guarantees of subsystems. We are ultimately striving to relate top-level requirements, such as on performing coordinated vehicle maneuvers to avoid collisions, to worst-case execution times of tasks implementing control functions for such maneuvers.