Servicenavigation

Project Details

Back

Projekt Print View

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
 
Final Report Year 2017

Final Report Abstract

The Transregional Collaborative Research Center AVACS focused on rigorous, highly automated methods and algorithms for the analysis and verification of what would today be called complex Cyber-Physical Systems, in which software and hardware implement algorithms for highly automated control of physical systems such as aircrafts, cars, trains, or systems of these. Within the twelve years spanned by AVACS, we have seen the projected exponential take-up of embedded systems, creating seemingly intelligent systems, capable of autonomous decision-making, both in the transportation domain targeted by AVACS, but also in other industrial sectors such as enabling smartness in smart grids, smart homes, smart cities, smart crisis management etc. Common to all is the increasing degree of delegation of decision making from humans to technical systems. Thus the need identified by AVACS at its conception, to “verify compliance of embedded control to reliability, coordination, control and real-time requirements”, and hence the relevance of AVACS results has drastically increased during its 12 year funding period. Virtually all industrial domains will be dependent on (large scale networks of) such highly autonomous systems, and thus guaranteeing their correctness and availability is of extreme industrial and societal relevance. AVACS addressed in its three research areas of real-time systems, hybrid systems, and systems of systems fundamental challenges in the verification and analysis of such Systems of Cyber-Physical Systems. Through the solutions created in this creative research environment, • we understand the mathematical essence of Systems of Cyber-Physical Systems and have mathematical models allowing in principle a complete formalization of multi-layered design of such systems; • we understand the principles of the design of such Systems of Cyber-Physical Systems, in that we can provide guidelines for building such systems enabling the use of decomposition techniques, compositional reasoning, and abstraction for reducing the complexity of the verification problem; • we understand the expressivity of logics required to capture coordination, control, reliability and real-time requirements, as well as various other industrially relevant types of requirement, and have investigated the complexity of such logics and – if applicable – decision procedures; • we master a broad class of verification and formal synthesis approaches defining the state of the art for the verification of such complex systems. While research in the first funding phase focused in isolation on the analysis of real-time systems, hybrid systems, and systems of systems, the cross fertilizations of results across research areas achieved by AVACS manifests itself in verification techniques for highly complex models, such as in the analysis of probabilistic hybrid automata with non-linear dynamics, for the analysis of probabilistic hybrid topologylabeled game structures, the analysis of dynamically communicating ensembles of linear hybrid automata, and the analysis of parametrically generated real-time systems with complex types. Model classes proven to be undecidable were shown nonetheless to be amenable to complete verification methods by exploiting guidelines generally accepted in industry, such as those for robust system design. AVACS has played a leading role in systematically advancing the state of the art in arithmetic SMT solving, enhancing both its scalability and its coverage of unprecedentedly rich fragments of arithmetic and logic. Numerous transfer activities are taking the foundational results of AVACS closer to industrial application. This can and will continue to be successful, when principles of design for analyzability as developed by AVACS are adhered to. Only if such design principles are observed, can the results of AVACS contribute to building predictable and robust smart systems.

Publications

 
 

Additional Information

© 2024 DFG Disclaimer / Copyright / Privacy Policy

Textvergrößerung und Kontrastanpassung