CAREER:Robust Verification of Cyber-Physical Systems

Abstract: 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. New cross-disciplinary courses at the undergraduate and graduate levels in hybrid control system design and analysis will be developed and taught. Activities for pre-college students involving programming with physical systems will be conducted towards increasing their interest in STEM related careers. Undergraduates, especially those from minority and underrepresented groups, will be recruited and mentored through involvement in research and outreach activities. The success of this research will force a quantum jump in the existing verification methodologies for CPSs, in particular, in the domains of automotive and aerospace systems, by bridging the gap in the analyses at the design and implementation phases.