A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms"

• ABSTRACT:
  
  We describe some inconsistencies in John Rushby's axiomatization of time-triggered algorithms that he presented in these transactions and that he formally specifies and verifies in the mechanical theorem-prover PVS. We present corrections for these inconsistencies that have been checked for consistency in PVS.

• BIBTEX:
  

  @article{pike_tse06,
   author    = {Lee Pike},
   title     = {A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms"},
   journal   = {IEEE Transactions on Software Engineering},
   volume    = {32},
   number    = {5},
   month     = {May},
   year      = {2006},
   pages     = {347--348},
   publisher = {IEEE Computer Society},
   note      = {Available at \url{http://www.cs.indiana.edu/~lepike/pub_pages/time_triggered.html}}}
  
  

• PAPER DOWNLOAD: pdf

• PVS FILES DOWNLOAD: Rushby's Mended Specifications, with a Theory Interpretation
  File commented: 'old' specifications are the ones in the original file and 'new' specifications are the fixed axioms. Mended proofs are marked as 'mended'.