The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - May (2006 vol.32)
pp: 347-348
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.
INDEX TERMS
Formal methods, formal verification, time-triggered algorithms, synchronous systems, PVS.
CITATION
Lee Pike, "A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms'", IEEE Transactions on Software Engineering, vol.32, no. 5, pp. 347-348, May 2006, doi:10.1109/TSE.2006.41
17 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool