GRK 2428:  CONVEY - Continuous Verification of CYber-Physical Systems

• Subject Area: Computer Science
• Term: since 2019
• Website: Homepage
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 378803395

Within the last few years, networks, computers, sensors, and actuators have been increasingly integrated into cyber-physical systems, i.e., software systems that interact with the physical world and must cope with its continuous behavior. Cyber-physical systems have reached an overwhelming complexity, which creates a host of challenges and research opportunities for software science, classical control theory, and informatics at large. In addition, in recent years, methods from artificial intelligence have started to play a crucial role in cyber-physical systems. As many of these systems are safety-critical, their design and deployment should ideally be accompanied by extensive sanitization, if not verification of their behavior, based on a rigorous semantic foundation. The integration of artificial intelligence has created extra challenges to this task. Within the first funding period, we have considered some aspects of the integration of artificial intelligence, in particular machine learning. In the second funding period, we plan to strengthen this direction to explore techniques for designing or formally verifying AI-enabled systems that interact with a changing environment. Change is a fundamental challenge in the verification of cyber-physical systems, be they AI-enabled or not, setting them apart from other data- or software-intensive systems: (1) The requirements change. While in other software areas, most change requests target at new or different functional behavior, AI-enabled cyber-physical systems designers also face increasingly frequent, non- functional change requests, e.g., for faster response time and lower power consumption. (2) The available knowledge changes, or even the whole implementation. While the former may be due to data acquisition or learning, the latter may undergo modification due to refactoring, or new hardware. (3) The physical environment changes continuously, in ways that cannot be completely foreseen at the design stage, and the system should adapt to these changes on its own. This introduces a third dimension of change, qualitatively different from the previous ones. Future technology for rigorous design and verification of AI-enabled cyber-physical systems will have to address continuous data, continuous behaviour, continuous development, continuous learning, and continuous analysis and synthesis at the same time. Verification techniques for taking AI-enabled components into account, though, are still in their infancy. Handling change at the requirement, implementation, and environment levels for AI-enabled cyber-physical systems requires a marriage between control theory, artificial intelligence, and formal methods. Only then will it be possible to realize AI-enabled cyber-physical systems, such as advanced medical devices, human-friendly robots, and autonomous vehicles operating in public spaces.

• DFG Programme: Research Training Groups
• Applicant Institution: Ludwig-Maximilians-Universität München
• Co-Applicant Institution: Technische Universität München (TUM)
• Spokesperson: Professor Dr. Dirk Beyer
• Participating Researchers: Professorin Dr. Susanne Albers; Professor Dr.-Ing. Matthias Althoff; Professor Dr. Jasmin Christian Blanchette; Professor Dr. Javier Esparza; Professor Debarghya Ghoshdastidar, Ph.D.; Professorin Dr. Marie-Christine Jakobs; Professor Dr. Johannes Kinder; Professor Jan Kretinsky, Ph.D.; Professorin Dr. Angela Schoellig; Professor Dr. Majid Zamani