In recent years, the idea of the model-based design paradigm is to develop design models and subject them to early analysis, testing, and validation prior to their implementation. Simulation-based testing ensures that a finite number of user-defined system trajectories meet the desired specification. Even though computationally inexpensive simulation is ubiquitous in system design, it suffers from incompleteness, as it is impossible or impractical to test all system trajectories. On the other hand, verification methods enjoy completeness by showing that all system trajectories satisfy the desired property. This project brings together leading experts in embedded control, hybrid systems, and software monitoring and testing to develop the foundations of a modern framework for testing the robustness of embedded hybrid systems. The central idea that this project is centered around is the notion of a robust test, where the robustness of nominal test can be computed and used to infer that a tube of trajectories around the nominal test will yield the same qualitative behavior.

Sensor topologies for minimal planning (DARPA SToMP)

Embedded systems require very novel, very challenging specifications that have to deal with synchronization, sequencing, and temporal ordering of different tasks. Mathematically formulating such desired specifications cannot be achieved using traditional mathematical formulations in control theory. On the other hand, computer aided verification has popularized the use of several temporal logics to describe complex specifications. However, the emphasis has been on verification of these properties for purely discrete systems, and not on synthesis for systems with a continuous component. In this research, a novel approach for automatically synthesizing hybrid controllers is pursued in order to satisfy specifications that are expressed in temporal logics. The proposed framework will provide algorithms and tools for the computation of discrete controllers, which by refinement will lead to embedded, hybrid controllers for the original system while providing performance and correctness guarantees.

Multi-robot emergency response (NSF ITR)

This project, in collaboration with the University of Minnesota and the California Institute of Technology, addresses research issues key to an important application of robot teams and information technology (emergency response in hazardous environments for various tasks). The research focuses on the development of methods for team coordination and dynamic distribution of tasks to robots. The project integrates the algorithms with first responder teams, emphasizing realistic scenarios.

Formal analysis and design of hybrid systems (NSF ITR)

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.

Adaptive coordinated control of intelligent multi-agent teams (ARO MURI)

This multi-university project involves the University of Pennsylvania, the University of California at Berkeley, and Carnegie Mellon University. It focuses on the design and evaluation of the adaptive hierarchical control of mixed autonomous and human operated semi-autonomous teams that deliver high levels of mission reliability despite uncertainty arising from rapidly evolving environments and malicious interference from an intelligent adversary. The design of architectures combining both hierarchical and heterarchical elements, the analytical foundations of interacting hybrid systems, the design of controllers for such systems that are robust against uncertainty, the management of rich sensory information from networked sensors among distributed and mobile teams; and the incorporation of human intervention in a mixed-initiative system are all key areas of our work. Additionally, the novelty of our approach is to explicitly take into account the need to adaptively replan missions to take into account environmental uncertainties and the deliberate malicious actions of a determined adversary. Equipment for this project is supported by an ARO DURIP grant.

Hierarchical abstractions of hybrid systems (NSF CAREER, PECASE)

Hybrid systems provide a theoretical foundation for the modeling, analysis, and design of embedded systems. Hybrid systems naturally combine discrete-event and continuous-time systems in a manner that can capture software logic, physical dynamics, and communication protocols, in a unified modeling framework. The wide applicability of hybrid systems has inspired a great deal of research from both control theory and theoretical computer science. Despite the great success of hybrid systems as a model, the applicability of state-of-the-art analysis and design techniques for hybrid systems has been limited to examples of small size due to complexity. Tthe research and educational agenda of the proposed research focuses on developing the theoretical foundations for the hierarchical decomposition of hybrid systems at various levels of abstraction. The long term goal of the research agenda will address the fundamental problem of given a class of hybrid models, and a class of properties that must be preserved, extract modeling abstractions that preserve the properties of interest. Achieving this goal will consist of first developing robust notions of bi-simulation for purely continuous systems, and then unifying the continuous and discrete notions in a manner that is consistent with the dynamics of hybrid systems.

Model based integration of embedded software (DARPA MoBIES)

The objective of this project is to develop a methodology and toolkit for design of embedded software for multi-agent communicating hybrid systems. The methodology will cover various design stages, including modeling, simulation, analysis, implementation, and monitoring. The methodology will be based on formal modular and hierarchical semantics of multi-agent hybrid systems. The methodology will improve the process for hybrid systems design by decreasing development costs through high-level modeling, by improving reusability by means of modular designs, and by developing more reliable designs with the help of analysis and runtime valiadation.