A note on inconsistent axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms"
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 verification time-triggered algorithms pvs formal methods synchronous systems