SRI

PROBABILISTIC, COMPOSITIONAL, MULTI-DIMENSION MODEL-BASED VERIFICATION (PROMISE) 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: 1. Probabilistic certification tools and 2. A composition framework to calculate system-level probabilistic certificates from component-level certificates. DARPA META PROMISE (PRObabilistic, Compositional MultI-Dimension Model-BaSEd 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. Grit Denker, Linda Briesemeister, Daniel Elenius, Shalini Ghosh, Ian Mason, Ashish Tiwari 
SRI International Devesh Bhatt, Haftay Hailu, Gabor Madl, Siamak Nikbin, Srivatsan Varadarajan 
Honeywell Aerospace Guenther Bauer, Wilfried Steiner 
TTTech Computertechnik AG Xenofon Koutsoukos, Tihamer Levendovszky 
Vanderbilt University
file

Visible to the public CyPhyHiLITEv2.zip

file

Visible to the public hsalRelAbsV4.zip