loading...
  • 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
ASCII Text
x 
 
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.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2006.41,
author = {Lee Pike},
title = {A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms'},
journal ={IEEE Transactions on Software Engineering},
volume = {32},
number = {5},
issn = {0098-5589},
year = {2006},
pages = {347-348},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2006.41},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms'
IS - 5
SN - 0098-5589
SP347
EP348
EPD - 347-348
A1 - Lee Pike,
PY - 2006
KW - Formal methods
KW - formal verification
KW - time-triggered algorithms
KW - synchronous systems
KW - PVS.
VL - 32
JA - IEEE Transactions on Software Engineering
ER -
 
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.