Title :
A note on inconsistent axioms in Rushby\´s "systematic formal verification for fault-tolerant time-triggered algorithms"
Author_Institution :
Galois Connections, Beaverton, OR
fDate :
5/1/2006 12:00:00 AM
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
Keywords :
formal specification; formal verification; software fault tolerance; theorem proving; John Rushby axiomatization; PVS mechanical theorem-prover; fault-tolerant computing; formal specification; systematic formal verification; time-triggered algorithms; Clocks; Conferences; Error correction; Fault tolerant systems; Floors; Formal specifications; Formal verification; Real time systems; Formal methods; PVS.; formal verification; synchronous systems; time-triggered algorithms;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.2006.41
