DARPA’s META program funded research to significantly improve the design, manufacture, and verification of complex cyber-physical systems. This project directly addressed that goal by allowing the system architecture to be composed from libraries of complexity reducing design patterns with formally guaranteed properties. This allows new system designs to be developed rapidly using patterns that have been shown to reduce unnecessary complexity and coupling between components. This work also deeply embeds formal verification into the design process to enable correct-by-construction development of systems that work the first time. The use of components with formally specified contracts, design patterns that provide formally guaranteed properties, and an architectural modeling language with a formal semantics ensures that the system design is known to meet its requirements even before it is implemented.
Rockwell Collins and our teammates, the University of Illinois at Urbana-Champaign (UIUC), the University of Minnesota (UMN), and the WW Technology Group (WWTG), addressed these challenges by developing capabilities in three key areas:
- Complexity-reducing system design patterns with formally guaranteed properties, supporting correct-by-construction composition of system designs
- Architectural modeling and analysis to support virtual integration, composition, and verification of system-level properties
- Automated formal verification deeply embedded in the system design process in order to prevent errors, resulting in dramatic schedule efficiencies