CPS: Small: Sound Invariant Generation for Continuous and Hybrid Systems

点击翻译按钮获取中文摘要

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/