| タイトル | Diagnosing a Failed Proof in Fault-Tolerance: A Disproving Challenge Problem |
| 本文（外部サイト） | http://hdl.handle.net/2060/20060046664 |
| 著者（英） | Torres-Pomales, Wilfredo; Miner, Paul; Pike, Lee |
| 著者所属（英） | NASA Langley Research Center |
| 発行日 | 2006-01-01 |
| 言語 | eng |
| 内容記述 | 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. |
| NASA分類 | Computer Programming and Software |
| 権利 | Copyright, Distribution as joint owner in the copyright |
