Loading...
Please wait, while we are loading the content...
Similar Documents
Model checking failed conjectures in theorem proving: a case study
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Miner, Paul Pike, Lee Torres-Pomales, Wilfredo |
| Copyright Year | 2004 |
| Description | Interactive mechanical theorem proving can provide high assurance of correct design, but it can also be a slow iterative process. Much time is spent determining why a proof of a conjecture is not forthcoming. In some cases, the conjecture is false and in others, the attempted proof is insufficient. In this case study, we use the SAL family of model checkers to generate a concrete counterexample to an unproven conjecture specified in the mechanical theorem prover, PVS. The focus of our case study is the ROBUS Interactive Consistency Protocol. We combine the use of a mechanical theorem prover and a model checker to expose a subtle flaw in the protocol that occurs under a particular scenario of faults and processor states. Uncovering the flaw allows us to mend the protocol and complete its general verification in PVS. |
| File Size | 247698 |
| Page Count | 18 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20040191341 |
| Archival Resource Key | ark:/13960/t05x78t7r |
| Language | English |
| Publisher Date | 2004-10-01 |
| Access Restriction | Open |
| Subject Keyword | Numerical Analysis Theorem Proving Formalism Protocol 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 |
