Actions for Diagnosing a Failed Proof in Fault-Tolerance : A Disproving Challenge Problem

Email RIS file
Bookmark
Report an Issue

Diagnosing a Failed Proof in Fault-Tolerance : A Disproving Challenge Problem

Author
Torres-Pomales, Wilfredo
Published
[2006].
Physical Description
1 electronic document
Additional Creators
Miner, Paul and Pike, Lee
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
This paper proposes a challenge problem in disproving. We describe a fault-tolerant distributed protocol designed at NASA for use in a fly-by-wire system for next-generation commercial aircraft. An early design of the protocol contains a subtle bug that is highly unlikely to be caught in fault injection testing. We describe a failed proof of the protocol's correctness in a mechanical theorem prover (PVS) with a complex unfinished proof conjecture. We use a model checking suite (SAL) to generate a concrete counterexample to the unproven conjecture to demonstrate the existence of a bug. However, we argue that the effort required in our approach is too high and propose what conditions a better solution would satisfy. We carefully describe the protocol and bug to provide a challenging but feasible case study for disproving research.
Other Subject(s)
Collection
NASA Technical Reports Server (NTRS) Collection.
Note
Document ID: 20060046664.
DISPROVING 06- 3rd Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability; 16 Aug. 2006; Seattle, WA; United States.
Terms of Use and Reproduction
Copyright, Distribution as joint owner in the copyright.
View MARC record | catkey: 16003287