Embedded systems, such as controllers in automotive, medical, and avionic systems, consist of a collection of interacting software modules reacting to and controlling an analog environment. Engineering disciplines such as control theory focus on continuous dynamics, and offer foundations for designing robust control laws for ensuring optimal performance of dynamical systems. Computing disciplines such as software engineering focus on discrete programs, and offer structured ways of implementing complex control and analysis tools for validating distributed software. For networked embedded devices with multiple modes of operation, the combination of the complexity in both discrete and continuous aspects leads to fundamental problems that are not yet well understood, and this makes the programming of reliable embedded systems a particularly challenging task. A systematic approach to designing embedded devices requires combining tools from control theory and modern software engineering, and the emerging theory of hybrid systems---systems with tightly integrated discrete and continuous dynamics, has the potential to provide the foundation. Despite the great appeal of hybrid systems as a model, the applicability of the state-of-the-art analysis and design techniques for hybrid systems has been limited to examples of small size due to complexity. This ITR research aims to develop foundations and tools for automatic abstraction and hierarchical decomposition as a means of simplification and scalability.
To facilitate high-level design of embedded software, modeling concepts such as hierarchy, modularity, reuse, compositionality, and object-orientation, are explored to 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.
