Complexity-Reducing Design Patterns for Cyber-Physical Systems

This report describes a design flow and supporting tools to significantly improve the design, manufacture, and verification of complex cyber-physical systems 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.