Compositional Analysis of Autonomous Systems
Abstract
Cyber-physical systems (CPS) consist of interacting computational and physical components. Autonomous systems such as autonomous cars, trains and factories are prominent examples of CPS. As CPS are becoming continuously larger in size, more complex in functionality, and more safety-critical in their applications, it is vital to guarantee their safety and correctness. This project aims at developing innovative verification techniques to assure safe behavior of cyber-physical systems. Hybrid systems are mathematical models that combine discrete and continuous dynamics, which makes them particularly suitable to model CPS. Although tremendous progress in terms of analysis scalability has been made in the last decade, available hybrid model checkers still lack the scalability to analyze large networked systems, i.e., composite hybrid systems consisting of multiple components. In other words, all available tools do not provide any special treatment for composite systems, whereas industry relevant models, e.g. the ones modeled in MathWorks Simulink, usually consist of multiple components. In this project, we will focus on this problem and develop novel techniques for compositional analysis of hybrid systems, i.e., we will look how to decompose the verification of a system into the verification of its components, which are smaller and therefore easier to verify.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Apr 09, 2018
- Source ID
- FA23861714065
Entities
People
- Sergiy Bogomolov
Organizations
- Air Force Office of Scientific Research
- Australian National University
- United States Air Force