The challenge in designing reliable and adaptable cyber-physical systems (CPSs) is rooted in the complexity of systems that combine a range of functions covering closed- and open-loop control modules. Control modules operate in the context of failure-prone sensors and actuators, integrated computing and hardware platforms, networked systems of systems, and physical environments. Verification methods for CPSs must address the broad range of mathematical models for computational and physical entities.
Verification techniques are computation-cost prohibitive if applied uniformly to each detail of a large, complex CPS design. It becomes necessary to decompose the verification space into appropriate abstractions, and trade-off specificity for tractability in principled ways, or approximate with probabilistic approaches in order to verify large-scale designs
The main technological verification barriers to realizing a
"correct-by-construction" approach to large-scale CPSs are as follows:
- Probabilistic certification tools and
- A composition framework to calculate system-level probabilistic certificates from component-level certificates.
DARPA META PROMISE (
PRO babilistic, Compositional
Mult
I-Dimension Model-Ba
SEd Verification) developed tools and a composition framework to address both challenges. The PROMISE team is led by SRI International and includes Honeywell International Inc., TTTech Computertechnik AG, and Vanderbilt University. PROMISE builds on the team's unique expertise that combines a long history of successful applications of formal verification tools with expertise and technology for aerospace safety design, certification and reliable and cost-effective manufacturing.
The PROMISE verification framework enables verifying CPS-level behavior and safety properties by using the composition of pre-certified components. By capturing the architectural assumptions and patterns in the reasoning framework that provide design-level certificates, both the depth and scalability of the analysis is significantly improved. This allows probabilistic certification of aircraft-level design with minimal real-world testing. It also enables verifying designs composed with heterogeneous architectural elements and networking configurations, including the verification of integrated compositions of software-control algorithms and electromechanical components, and the verification of mixed synchronous and asynchronous designs on the aircraft-level integrated networks.
PROMISE has developed verification techniques, methodologies and tools in the following four areas:
- Probabilistic Network Fault and Performance Analysis
- Compositional Verification of Hybrid Dynamical Systems
- Probabilistic Failure Analysis
- Integrated Design Flow and Verification