Project Details
Projekt
TRR 14: Automatic Verification and Analysis of Complex Systems
Subject Area
Computer Science, Systems and Electrical Engineering
Term
from 2004 to 2015
Project identifier
Deutsche Forschungsgemeinschaft (DFG) - Project number 5485999
This project addresses the rigorous mathematical analysis of models of complex safety critical computerised systems, such as aircrafts, trains, cars or other artifacts, whose failure can endanger human life.
The aim is to raise the state of the art in automatic verification and analysis techniques 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. 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, the project should 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 modelling 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 are not found in present verification systems.
The aim is to raise the state of the art in automatic verification and analysis techniques 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. 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, the project should 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 modelling 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 are not found in present verification systems.
DFG Programme
CRC/Transregios
International Connection
Czech Republic
Completed projects
- H01 - Deduction and Automata Based Approaches (Project Head Ganzinger, Harald )
- H02 - Bounded Model Checking and Inductive Verification of Hybrid Systems (Project Head Becker, Bernd )
- H02 - Constaint-based Verification for Hybrid Systems (Project Heads Althaus, Ernst ; Becker, Bernd ; Fränzle, Martin ; Weidenbach, Christoph )
- H03 - Automated Verification of Cooperating Traffic Agents (Project Heads Althaus, Ernst ; Damm, Werner ; Olderog, Ernst-Rüdiger ; Scholl, Christoph ; Sofronie-Stokkermans, Viorica ; Waldmann, Uwe )
- H04 - Automatic Verification of Hybrid System Stability (Project Heads Fränzle, Martin ; Hermanns, Holger ; Podelski, Andreas ; Theel, Oliver ; Wolf, Verena )
- R01 - Beyond Timed Automata (Project Heads Finkbeiner, Bernd ; Fränzle, Martin ; Olderog, Ernst-Rüdiger ; Podelski, Andreas ; Sofronie-Stokkermans, Viorica )
- R02 - Timing Analysis, Scheduling and Distribution of Real-Time Tasks (Project Heads Althaus, Ernst ; Damm, Werner ; Hack, Sebastian ; Reineke, Jan ; Wilhelm, Reinhard )
- R03 - Heuristic Search and Abstract Model Checking (Project Heads Finkbeiner, Bernd ; Nebel, Bernhard ; Podelski, Andreas )
- S01 - Compositional Approaches to System Verification (Project Heads Becker, Bernd ; Finkbeiner, Bernd ; Nebel, Bernhard ; Scholl, Christoph )
- S02 - Dynamic Communication Systems (Project Heads Damm, Werner ; Finkbeiner, Bernd ; Hermanns, Holger ; Podelski, Andreas ; Weidenbach, Christoph )
- S03 - Verification of Dependability Properties (Project Heads Becker, Bernd ; Hermanns, Holger ; Theel, Oliver ; Wolf, Verena )
- T01 - Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving (DeCoDe) (Project Heads Becker, Bernd ; Fränzle, Martin )
- Z01 - Central Tasks (Project Heads Becker, Bernd ; Damm, Werner ; Finkbeiner, Bernd )
Applicant Institution
Carl von Ossietzky Universität Oldenburg
Co-Applicant Institution
Albert-Ludwigs-Universität Freiburg; Universität des Saarlandes
Participating Institution
Max-Planck-Institut für Informatik
Spokesperson
Professor Dr. Werner Damm
