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 integrate 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 Caltech web sites.

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.

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:

  1. Hybrid and embedded systems theory.
  2. Model-based software design/verification.
  3. Composable Tool Architectures.
  4. Testing and Experimental Validation.
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.

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.

2008 High-Confidence Design for Distributed Embedded Systems (HCDDES) Review Meeting

The 2008 High-Confidence Design for Distributed Embedded Systems (HCDDES) Review Meeting occurred on October 14, 2008 at UC Berkeley.

Joint Review Meeting of MURI Projects on High-Confidence Design for Distributed Embedded Systems: September 6, 2007

On September 6, 2007, we held a review meeting for the Caltech/MIT/University of Washington project on Specification, Design and Verification of Distributed Embedded Systems and the Vanderbilt/Berkeley/CMU/Stanford project on Frameworks and Tools for High-Confidence Design of Adaptive, Distributed Embedded Control Systems.
  • Agenda
  • HCDDES Presentations:
  • Janos Sztipanovits. High-Confidence Design for Distributed Embedded Systems MURI Project Overview
  • Claire Tomlin, S. Shankar Sastry. Robust Hybrid and Embedded Systems Design for Quadrotor Platform
  • Stephen Boyd. Controller Coefficient Truncation Using Lyapunov Performance Certificate
  • Bruce Krogh. Embedded Systems Modeling and Deep Compositionality
  • Edward A. Lee. Principled Design of Embedded Systems
  • Peter Volgyesi, Gabor Karsai, Janos Sztipanovits. Toward a Model-Based Tool Chain for High Confidence Design
  • Flavio Lerda, Edmund M. Clarke. Source Code Verification and Testing
  • Gabe Hoffmann. STARMAC The Stanford Testbed of Autonomous Rotorcraft for Multi-Agent Control
  • 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 system specification.

    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 required testing.

    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.

    CVS Access

    To get CVS access, you must first get a Chess website account in this workgroup (hcddes) and then request a separate cvs account:

    1. Request an account in the hcddes workgroup
      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.
    2. After your hcddes workgroup account is created, go to Options -> Request CVS Account
    3. Check out the repository.
      Users running bash:
      export CVS_RSH=ssh
      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?
    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 starmac repository is restricted by Unix group permission. Access will only be granted to HCDDES participants.
    1. Request CVS Account
    2. Send email to Christopher asking to be added to the starmac Unix group on source.eecs
    3. To check out the tree:
      cvs -d :ext:source.eecs.berkeley.edu:/home/cvs_chess co starmac
    ©2002-2018 Chess