Sound Invariant Generation for Continuous and Hybrid Systems
Lead PI:
Andre Platzer
Abstract
This project considers the pragmatic challenge of broadening the reach and general accessibility of cyber-physical system (CPS) analysis. It capitalizes on logical foundations for cyber-physical systems to study automated analysis for CPS without sacrificing correctness of the analysis results. While the complexities of CPSs can be quite demanding, there is a considerable pragmatic difference between rigorous reasoning techniques that are available to verification experts compared to techniques that provide a vast amount of automation support to become more accessible for novices and more productive for experts. This project focuses on finding invariants, which convey crucial insights about quantities or relationships, such as minimum safety distances, that do not change while the CPS drives or flies. Cyber-physical systems such as self-driving cars, advanced computerized car safety technology, and drones have considerable potential to change the world for the better. Their designs face intensive safety requirements, however, and feature increasingly complex behaviors. The advanced but correct automation of CPS analysis technology developed in this project is crucial to broaden the reach of trustworthy verification and validation results. In the long run, there is a chance that this technology will fundamentally change the way that CPS are engineered by enabling CPS engineers to have increasingly comprehensive safety analysis tools at their fingertips. As a demonstration with considerable impact potential, this project studies safe control functionalities for quadrotors. Quadcopters are a popular choice for realizing many applications, but their safety is a nontrivial challenge. Not every company or grass-roots effort will have the capacity to conduct a full verification and validation effort. That is why a set of baseline functionalities that have been preverified are expected to be a helpful basis for such designs. The results of this project, including CPS models, controllers, proofs, and tools, will be made available on the KeYmaera X web page: http://keymaeraX.org/
Andre Platzer

André Platzer is a Professor of Computer Science at Carnegie Mellon University, Pittsburgh, PA, USA. He develops the Logical Foundations of Cyber-Physical Systems (NSF CAREER). In his research, André Platzer works on logic-based verification and validation techniques for various forms of cyber-physical systems, including hybrid systems, distributed hybrid systems, and stochastic hybrid systems. He developed differential dynamic logic and differential invariants and leads the development of the CPS verification tool KeYmaera X.

André Platzer received an ACM Doctoral Dissertation Honorable Mention Award, an NSF CAREER Award, and was named one of the Brilliant 10 Young Scientists by the Popular Science magazine 2009 and one of the AI's 10 to Watch 2010 by the IEEE Intelligent Systems Magazine.

Performance Period: 09/01/2017 - 08/31/2020
Institution: Carnegie-Mellon University
Sponsor: National Science Foundation
Award Number: 1739629