• Publication
  • 2006
  • Issue No. 5 - May
  • Abstract - A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms'
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms'
May 2006 (vol. 32 no. 5)
pp. 347-348
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.

[1] J. Rushby, “Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms,” IEEE Trans. Software Eng., vol. 25, no. 5, pp. 651-660, Sept. 1999.
[2] S. Owre, J. Rusby, N. Shankar, and F. von Henke, “Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS,” IEEE Trans. Software Eng., vol. 21, no. 2, pp. 107-125, Feb. 1995.
[3] S. Owre and N. Shankar, “Theory Interpretations in PVS,” Technical Report SRI-CSL-01-01, SRI Int'l, Apr. 2001, http://pvs.csl.sri.com documentation.shtml .
[4] J. Rushby, “Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms,” Dependable Computing for Critical Applications— 6, vol. 11, pp. 203-222, Mar. 1997.

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
Usage of this product signifies your acceptance of the Terms of Use.