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

摘要

I describe some inconsistencies in John Rushby s axiomatization of time-triggered algorithms that he presents in these transactions and that he formally specifies and verifies in a mechanical theorem-prover. I also present corrections for these inconsistencies.