High-level design of embedded software requires modeling concepts such as hierarchy, modularity, reuse, compositionality, and object-orientation. In this project we will develop a theory of hierarchical hybrid systems with an accompanying a compositional calculus of refinement. This will be the basis for behavioral interfaces and descriptions of components at different levels of abstractions. For rigorously specifying and evaluating design alternatives and correctness requirements, automated techniques such as model checking are very effective. To apply these techniques for formal analysis of hybrid systems, this research is developing automated schemes for constructing abstractions of hybrid models. The technical directions being pursued include model checking algorithms that exploit hierarchy, algorithms for extracting finite-state approximations using predicate abstraction, counter-example guided refinement of abstractions, property-preserving bisimulation-based reductions of continuous differential equations, and assume-guarantee reasoning. The results of this research are being integrated in software tools for modeling and analysis of hybrid systems. The benefits of the techniques for developing embedded systems with higher assurance for safety and reliability are evaluated in an experimental testbed of multiple, autonomous, mobile robots.
Description