Specification, Design and Verification
of Distributed Embedded Systems
|Mani Chandy John C. Doyle Richard M. Murray (PI)|
|California Institute of Technology|
|Eric Klavins||Pablo Parrilo|
|University of Washington||Massachusetts Institute of Technology|
Welcome to VaVMURI. This wiki has been set up to document the activities of our 2006 MURI project. If you are a member of the project team and would like to be able to edit pages on this wiki, send e-mail to Richard Murray and request an account. You are also invited to visit the wiki for our sister MURI, led by Vanderbilt.
We are investigating the specification, design and verification of distributed systems that combine communications, computation and control in dynamic, uncertain and adversarial environments. These systems consist of autonomous components (vehicles, sensors, communications nodes and command and control elements) that cooperate with each other and operate in environments with adversarial and random elements. The autonomous components collaborate by exchanging information and the bandwidth available for communication may be limited, for example when there is a great deal of ambient noise. Likewise, the computational and communication capability of components may vary based on the hardware, changing power constraints, or failures and repairs. Each autonomous component has a software-based control policy that governs its behavior as part of the overall system. This policy is based on the resources it has (e.g., power and computational capability) and the signals it receives from cooperating components, adversarial components and the noisy environment.
Our goal is to develop methods and tools for designing control policies, specifying the properties of the resulting distributed embedded system and the physical environment, and proving that the specifications are met. We partition the problem into three parts:
- Specification: How does the user specify--in a aingle formalism--continuous and discrete control policies, communications protocols and environment models (including faults)?
- Design and reasoning: How can engineers reason that their designs satisfy the specifications? In particular, can engineers reason about the performance of computations and communication, and incorporate real-time constraints, dynamics, and uncertainty into that reasoning?
- Implementation: What are the best ways of mapping detailed designs to hardware artifacts, running on specific operating systems? What languages are suitable for specifying systems so that the specifications can be verified more easily?
Our project focuses on the first two parts of the overall problem, with linkage to industry (Boeing) and national laboratories (JPL, AFRL) as a mechanism for transitioning the research results to implementation.