Robust Verification of Cyber-Physical Systems

Cyber-physical systems (CPSs) have become pervasive in the modern society, enabling transformative applications in the transportation, healthcare and energy sectors. However, the reliable development of CPSs remains an outstanding challenge. At the design level, hybrid systems theory provides a rich set of techniques and tools for ensuring correctness of high level functional properties such as safety and liveness. Current analysis techniques at the implementation level focus primarily on detecting low level runtime errors such as buffer overflows and divide by zero. A holistic approach to verifying functional specifications will considerably enhance the reliability scenario of CPSs development. This project investigates a robust verification methodology that guarantees functional correctness of the implementation by a "deeper" analysis on the design. More precisely, robust verification not only ensures that a design satisfies a given specification, but that small perturbations in the design still satisfy the specification. The perturbations on the design account for the deviations in the implementation with respect to the actual system. The proposed research investigates new foundations, abstractions and verification algorithms for robust analysis, in light of novel quantitative and/or topological aspects of robustness. In addition, prototype tools are developed to enable practical application and evaluation. The successful completion of the research will advance the knowledge in the fields of formal methods and hybrid control systems by leveraging ideas from control theory, dynamical systems theory, optimization theory and satisfiability modulo theory.