Comparative Analysis and VERification for Concurrent Correctness-Critical Systems (CAVER)

• Applicant: Professor Dr. Norbert Müller, since 7/2018
• Subject Area: Theoretical Computer Science
• Term: from 2014 to 2019
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 255389725

The increasing size and the networked and real-time nature of telecommunications, automatic controllers, web services, mobile and embedded devices, etc. confront us with the problem of the precise comprehension of their behavior and, hence, of the assurance of their correct functioning. The general approaches to cope with the problem are founded on rigorous formalisms and computer aided tools which can be helpful in the thorough modeling of the systems at all stages of their design and implementation. The project CAVER will work towards new and more efficient theoretical frameworks and software instruments that should be mathematically precise, designer-amicable, and able to expose sufficient details about the systems structures and behaviors, and thus join the existing effort of many other teams in the theory of concurrent and real-time systems. The combination of expertise in modeling, analysis, testing and verification of systems and applications that comes together in the CAVER team is perfectly suited for attacking theoretical and practical challenges in different aspects of concurrent correctness-critical systems (CCCS). We see our role in the following activities:The classification of formal models and unification of behavioral equivalences for CCCS, in order to get better understanding of the inherent concurrent, nondeterministic and timing nature of the system behavior and to strengthen the existing and derive new results based on the relationships between the individual models and equivalences.The elaboration and evolution of various verification methods for qualitative and quantitative reasoning about the behavior of CCCS, based on model checking and constraint solving techniques.Implementation and performance analysis for case studies, in order to implement, compare and evaluate the theoretical methods to be proposed and show their applicability and flexibility. The algorithms we will develop in the course of our research will be subject to experimentation, and lead to the development of prototypes.CAVERs research, even in its theoretical aspects, is driven by real-world problems, and is intended to promote emerging new methodologies for proving the systems correct and more generally for deriving their properties. There is hope that the practical consequences of the research may be extensive: the design of CCS might be improved, and their functioning might be made more reliable and safer.

• DFG Programme: Research Grants
• International Connection: Russia
• Partner Organisation: Russian Foundation for Basic Research
• Participating Persons: Professor Dr. Peter Buchholz; Dr. Margarita Korovina; Privatdozentin Dr. Louchka Popova-Zeugman; Dr. Igor Tarasyuk; Professorin Dr. Irina Virbitskaite
• Ehemaliger Antragsteller: Professor Dr. Eike Best, until 7/2018