Automatisierte Verifikation kooperierender Verkehrssysteme (TRR 14: AVACS - automatische Verifikation und Analyse komplexer Systeme)

In this project, methods and procedures for the mathematical analysis of models of complex safety-critical embedded systems are developed. Such systems are, for example, airplanes, trains, cars, or other artifacts whose failure can endanger lives. The goal is to improve the current state of the art of these methods, with which only individual aspects of such systems can be treated at a time (such as concurrency, timing, continuous control, stability, mobility, data structures, hardware constraints, modularity, levels of refinement), in such a way that comprehensive, holistic verification of these systems becomes possible.

By improving and increasing the automation of basic verification techniques (such as abstract interpretation, linear programming, constraint solving, Lyapunov functions, automatic decision procedures, automata-based verification, heuristic search) and by a deep, goal-oriented integration of these techniques, especially those models shall become treatable by automatic verification and analysis methods whose complexity still excludes this treatment today. Complexity here means system size as well as logical complexity induced by interferences between the different sub-aspects. By exploiting design paradigms (mathematically represented as decomposition theorems that divide complex systems into smaller, treatable subsystems or aspects), the combination of individual, complementary verification techniques will generate synergies that cannot be found in today's verification tools.