Actions for A Methodology for Evaluating Artifacts Produced by a Formal Verification Process

Email RIS file
Bookmark
Report an Issue

A Methodology for Evaluating Artifacts Produced by a Formal Verification Process

Author
Miner, Paul S.
Published
November 2011.
Physical Description
1 electronic document
Additional Creators
Person, Suzette and Siminiceanu, Radu I.
Online Version

Availability

I Want It
I Want It

Finding items...

Restrictions on Access
Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access
Summary
The goal of this study is to produce a methodology for evaluating the claims and arguments employed in, and the evidence produced by formal verification activities. To illustrate the process, we conduct a full assessment of a representative case study for the Enabling Technology Development and Demonstration (ETDD) program. We assess the model checking and satisfiabilty solving techniques as applied to a suite of abstract models of fault tolerant algorithms which were selected to be deployed in Orion, namely the TTEthernet startup services specified and verified in the Symbolic Analysis Laboratory (SAL) by TTTech. To this end, we introduce the Modeling and Verification Evaluation Score (MVES), a metric that is intended to estimate the amount of trust that can be placed on the evidence that is obtained. The results of the evaluation process and the MVES can then be used by non-experts and evaluators in assessing the credibility of the verification results.
Other Subject(s)
Collection
NASA Technical Reports Server (NTRS) Collection.
Note
Document ID: 20110022654.
NASA/TM-2011-217193.
L-20068.
NF1676L-13467.
Terms of Use and Reproduction
Copyright, Distribution as joint owner in the copyright.
View MARC record | catkey: 15981856