DocumentCode
969881
Title
A note on inconsistent axioms in Rushby\´s "systematic formal verification for fault-tolerant time-triggered algorithms"
Author
Pike, Lee
Author_Institution
Galois Connections, Beaverton, OR
Volume
32
Issue
5
fYear
2006
fDate
5/1/2006 12:00:00 AM
Firstpage
347
Lastpage
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
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;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/TSE.2006.41
Filename
1642681
Link To Document