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

• ABSTRACT:
  
  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.

• BIBTEX:
  

  @inproceedings{pike_disproving,
    author    = {Lee Pike and Paul Miner and Wilfredo Torres-Pomales},
    title     = {Diagnosing a Failed Proof in Fault-Tolerance: A Disproving Challenge Problem},
    booktitle = {DISPROVING 2006 Participants' Proceedings},
    year      = {2006},
    pages     = {24--33},
    note      = {Available at \url{https://leepike.github.io/pub_pages/disproving.html}}}
  

• PAPER DOWNLOAD: pdf 

• SLIDES DOWNLOAD: pdf

• FILES DOWNLOAD:
  
  
  • PVS files: PVS dump file
  • SAL file: SAL input file

• NOTES:
  
  This paper is a heavily revised and shortened version of a NASA Technical Memorandum by the same authors.

  ---

  Lee Pike (home)