High-Confidence Design of Adaptive, Distributed Embedded Control Systems (HCDDES)
The Multidisciplinary University Research Initiative (MURI) project on
High-Confidence Design for Distributed Embedded Systems
verification, validation, and test procedures throughout the complete
design, development and maintenance cycle, from requirements capture to
deployment and life cycle updates. This project is funded by the Air Force Office of Scientific Research. For details, see the Vanderbilt and
2009 High-Confidence Design for Distributed Embedded Systems (HCDDES) Review Meeting
The 2009 High-Confidence Design for Distributed Embedded Systems (HCDDES) Review Meeting
occurred on Wednesday, December 2, 2009 at UC Berkeley.
- Janos Sztipanovits. Frameworks
and Tools for High-Confidence Design of Adaptive,
Distributed Embedded Control Systems: Project
- Jerry Ding, Jeremey Gillula, Huang Haomiao, Michael Vitus,
Claire Tomlin. Robust
Hybrid and Embedded Systems Design
- Gabor Karsai, Joe Porter, Graham Hemingway and Janos Sztipanovits,
Model-Integrated Tool Chain for High Confidence Design
- Edward A. Lee. Correctly
Composing Components: Ontologies and Modal
- Andre Platzer, Edmund M. Clarke. Model-based
Testing and Verification of Embedded System
- Yang Wang. Performance
Bounds for Constrained Linear Stochastic
- Nicholas Kottenstette, Joe Porter. Constructive
Non-linear Control Design With Applications to Quad-Rotor
and Fixed-Wing Aircraft
The design of embedded systems is challenging for high-confidence aerospace systems, where technology leadership is the key to superiority. Next generation unoccupied air vehicles (UAVs) and space vehicles (SVs) are complex systems of systems involving multiple synchronous and asynchronous processes in an architecture distributed across several processors both within a single UAV (SV) and across groups of UAVs (SVs). Additionally, autonomy, fault tolerance, and resource optimization require that mixed-criticality functions are resident on the same processors in this architecture. Guaranteeing the provably correct behavior of the overall embedded system is extremely difficult, especially with respect to timing constraints and their relationship to safety of the physical systems, and performance specifications associated with mission-level objectives. Traditional software engineering methods cannot solve these problems because they do not address properties key to the interaction of physical processes with software, such as timing, mixed criticality functions, and concurrent processes.
This project is developing a comprehensive approach to the design of high-confidence complex embedded systems, that is, systems that are correct-by-construction, fault tolerant, secure, and degrade gracefully under fault conditions or information attack. Our approach integrates verification, validation, and test procedures throughout the complete design, development and maintenance cycle, from requirements capture to deployment and life cycle updates. This MURI project has the following research areas:
The CHESS component of this project is focused on an experimental quadrotor aircraft called the Starmac, shown below, designed by CHESS director Tomlin and her research group.
- Hybrid and embedded systems theory.
- Model-based software design/verification.
- Composable Tool Architectures.
- Testing and Experimental Validation.
Starmac team, left to right: Steven Waslander, Vijay Pradeep, Haomiao Huang, Michael Vitus and Gabe Hoffmann.
Jeremy Gillula is missing from the photo. All were Stanford graduate students or postdocs at the time.
BAA Announcement Number 05-017 describes the HCDDES project as:
FY06 MURI Topic #17
Submit white papers and proposals to the Air Force Office of Scientific Research
High Confidence Design for Distributed, Embedded Systems
Background: Prescribed safety and security is a significant challenge for current flight
management systems. Requirements, design, and test coverage and their quantification all
significantly impact overall system quality, but extensive software test coverage is
especially significant to development costs. For certain current systems, verification and
validation (V&V) comprise over 50% of total development costs. This percentage will be
even higher using current V&V strategies on emerging autonomous systems. Although
traditional certification practices have historically produced sufficiently safe and reliable
systems, they will not be cost effective for next-generation autonomous systems due to
inherent size and complexity increases from added functionality. New methods in high
confidence software combined with advances in systems engineering and the use of closed-
loop feedback for active management of uncertainty provide new possibilities for
fundamental research aimed at addressing these issues. These methods move beyond
formal methods in computer science to incorporate dynamics and feedback as part of the
Objective: Develop new approaches to designing/developing distributed embedded
systems to inherently promote high confidence, as opposed to design-then-test approaches
as prescribed by the current V&V process. Proposing teams should focus on developing new
design methods, analysis techniques, specification and integrated software
development/test environments that will radically lower V&V costs for future mixed critical
systems. The multidisciplinary team should include the necessary expertise in mathematics,
software architectures, security, modeling and simulation, fault tolerant systems, and
dynamics and control.
Research Concentration Areas: Areas of interest include, but are not limited to: (1)
formal reasoning about distributed, dynamic, feedback systems, including the application of
temporal logic and other tools from computer science and mathematics to reason about
real-time software. This applies to both cooperative and adversarial systems in distributed
computational environments; (2) development of relationships between system properties
and test coverage to reduce the required testing and provide improved efficiency, including
a mixture of automated testing and model-based reasoning to improve efficiency; (3)
development and analysis of architectures that provide behavior guarantees of online V&V.
Extend current methods for built-in-test (BIT) to higher levels of abstraction, including the
use of safety "wrappers" to insure that high performance code is replaced by safe code
when online monitors are triggered; (4) V&V aware architectures- techniques that are
designed to generate software and systems that are easier to verify and validate. Manage
V&V complexity instead of managing system functionality; (5) multi-threaded control: new
tools for reasoning about asynchronous, distributed processing common in multi-threaded
computational environments; and (6) approximate V&V-development of model-based
approaches to V&V that make use of simplifying approximations to improve V&V efficiency.
Develop relations of system analysis to the test vector generation to reduce/eliminate
Impact: Next-generation Unmanned Aerial Vehicles (UAVs) and unmanned space vehicles
will require advanced mixed critical system attributes to enable safe autonomous
operations. These emerging attributes will manifest themselves in all aspects of the system
including requirements, system architectures, software algorithms, and hardware
components. Development of new theory and algorithms for V&V will provide reduced
development time and cost, improved system functionality, and increased robustness to
uncertainty for new systems.
To get CVS access, you must first get a Chess website account in this workgroup (
and then request a separate cvs account:
Note that the Starmac code is in a separate CVS repository. There is a local copy at Berkeley of
a portion of the tree. Access to the Berkeley
- Request an account in the
Membership in this workgroup is restricted to people who are actively working on this project. Currently, our university partners are CMU, Stanford, Vanderbilt and UC Berkeley.
- After your
account is created, go to Options ->
Request CVS Account
- Check out the repository.
Users running bash:
cvs -d :ext:source.eecs.berkeley.edu:/home/cvs_chess hcddes
Users running csh:
setenv CVS_RSH ssh
cvs -d :ext:source.eecs.berkeley.edu:/home/cvs_chess hcddes
See also How do I check out my own tree?
starmac repository is restricted by
Unix group permission. Access will only be granted to
Request CVS Account
- Send email to Christopher
asking to be added to the
starmac Unix group
- To check out the tree:
cvs -d :ext:source.eecs.berkeley.edu:/home/cvs_chess co starmac
To modify this page, use CVS.