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.