A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms'
Issue No. 05 - May (2006 vol. 32)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2006.41
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.
Formal methods, formal verification, time-triggered algorithms, synchronous systems, PVS.
L. Pike, "A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms'," in IEEE Transactions on Software Engineering, vol. 32, no. , pp. 347-348, 2006.