Loading...
Please wait, while we are loading the content...
Similar Documents
A methodology for evaluating artifacts produced by a formal verification process
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Person, Suzette Siminiceanu, Radu I. Miner, Paul S. |
| Copyright Year | 2011 |
| Description | 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. |
| File Size | 388568 |
| Page Count | 28 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20110022654 |
| Archival Resource Key | ark:/13960/t6m093k28 |
| Language | English |
| Publisher Date | 2011-11-01 |
| Access Restriction | Open |
| Subject Keyword | Mathematical And Computer Sciences (general) Fault Tolerance Algorithms Ethernet Synchronism Mathematical Models Crew Exploration Vehicle Design Analysis Run Time Computers Formalism Program Verification Computers Ntrs Nasa Technical Reports ServerĀ (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |