The widespread prevalence of embedded devices, and networked collections of them, makes ensuring their reliability a social imperative. However, formal verification of such embedded systems is challenging as they are concurrent ``hybrid'' systems, i.e., coupled digital programs and physical entities that interact with an analog environment while meeting real-time constraints. Lured by the importance and scientific depth of the problem, the analysis of such hybrid systems for correctness has received widespread attention in the last couple of decades. Considerable progress has been made in defining languages and models for designing such systems, understanding the theoretical bounds to automated verification of such systems, and developing tools to simulate and verify formal hybrid models. However, key challenges remain. Current state of the art in formal methods allows for the automated analysis of single, closed hybrid systems with simple continuous dynamics. This is in contrast to the fact that, in practice, hybrid systems tend to have complex continuous dynamics, and usually consist of multiple modules interacting concurrently.
This work addresses these challenges so as to enable the automated analysis of systems that are open, concurrent, and hybrid. Specifically, the following research tasks will be carried out: (a) Develop techniques to tightly approximate hybrid systems with complex continuous dynamics by hybrid systems with simple dynamics; (b) Develop decision procedures for the composition of hybrid systems; (c) Develop assume-guarantee reasoning for hybrid systems in the presence of approximate abstractions; (d) Apply the proposed methods to analyze software and algorithms deployed in HoTDeC, an environment for distributed control of hovercrafts.
The widespread prevalence of embedded devices, and networked collections of them, makes ensuring their reliability a social imperative. The most convenient way to formally model such systems is as a hybrid system, as they are coupled digital programs and physical entities that interact with an analog environment while meeting real-time constraints. While considerable progress has been made in developing techniques for the analysis of hybrid systems, key challenges remain. Current state of the art allows for the automated analysis of single, closed hybrid systems with simple continuous dynamics. This is in contrast to the fact that, in practice, hybrid systems tend to have complex continuous dynamics, and usually consist of multiple modules interacting concurrently. To address these concerns, this project focused to developing techniques that transform a hybrid system with complex continuous dynamics into an abstract hybrid system with simpler continuous dynamics, such that verification of the abstract model establishes the correctness of the original system. Abstraction for two canonical properties were explored --- safety and stability. Informally, a safety property requires that nothing bad happens in any execution of the system, while stability specifies that all behaviors that start close to an equilibrium point stay close to that equilibrium point. For safety properties, we developed a counter-example guided abstraction-refinement (CEGAR) framework for hybrid systems. CEGAR is a technique that attempts to automatically construct a simple abstract model that will establish the correctness of a more complex system. This approach has been implemented in a research tool called HARE that is available for download. It has been well known that constructing abstract models to reason about safety can be based on the mathematical notion of simulation. However, we observed that stability cannot be reasoned in the same way. Thus, we came up with a new mathematical foundation for abstraction based reasoning of stability properties. We also developed new algorithms to automatically prove the stability of hybrid systems.
