Scalable algorithms for safety verification and reachability analysis of hybrid systems

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

In the past few decades, there have been tremendous advances in microprocessor technology and the use of digital controllers in the automation of physical plants. The increasing integration of such controllers results in highly complex systems involving both continuous and discrete event dynamics. In addition to discontinuities introduced by the computer, most physical processes exhibit discrete dynamics due to the action of elements ranging from valves, gears and switches in electromechanical systems to transcriptional regulators in genetic and metabolic networks. Such systems combining discrete and continuous features are called hybrid systems.Formal verification is a very important issue during system design. Its goal is to prove that the system performs as expected. As the automated systems are growing in scale and complexity, the possibility of subtle errors is much greater. This project develops scalable, provably correct algorithms and software tools for safety verification and reachability analysis of hybrid systems. First, the project investigates the construction of discrete abstractions. While doing this, this work attempts to enlarge the class of known decidable hybrid systems. Second, enabled by recent advances in semialgebraic methods and convex optimization, the project investigates a new method for safety verification that does not require explicit calculation of trajectories or reachable sets, and provides a nested family of sufficient conditions for system safety that are polynomial-time checkable. Third, bringing ideas from motion planning based on randomized techniques, the project develops an algorithm for test case generation.The algorithms developed in this project are implemented as a Reachability Analysis and VErification (Rave) toolkit and tested by considering two very difficult problems arising in the safety of multi-agent robotic systems. The results of this project also have an immediate impact in a wide range of areas where hybrid systems are used for modeling, such as automated highway systems, air-traffic management systems, genetic and metabolic networks, embedded automotive and avionic controllers, robotics, and real-time communication networks.