SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms (1997)
 by Dr. John Rushby.

An updated version of this paper was published in the IEEE Transactions on Software Engineering, Vol 25, No 5, September 1999.

Dependable Computing and Fault Tolerant Systems, Volume 11.
From Dependable Computing for Critical Applications—6.
Edited by Mario Dal Cin, Catherine Meadows and William H. Sanders.
IEEE Computer Society, Garmisch-Partenkirchen, Germany.
March, 1997.
Pages 203–222.


Abstract
Many critical real-time applications are implemented as time-triggered systems. We present a systematic way to derive a time-triggered implementation from a fault-tolerant algorithm specified as a functional program. It is relatively easy to formally and mechanically verify correctness and fault-tolerance properties of algorithms expressed in this latter form. The functional program is next transformed into an untimed synchronous system, and then to a time-triggered implementation. The second step is independent of the algorithm concerned and we prove its correctness; the proof has also been formalized and mechanically checked with the PVS verification system. This approach provides a methodology that can ease the formal specification and assurance of critical fault-tolerant systems.
BibTEX Entry
@INPROCEEDINGS{Rushby97:DCCA,
    AUTHOR = {John Rushby},
    TITLE = {Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms},
    VOLUME = {11},
    YEAR = {1997},
    PAGES = {203--222},
    MONTH = {mar},
    ADDRESS = {Garmisch-Partenkirchen, Germany},
    URL = {http://www.csl.sri.com/papers/dcca97/},
    SERIES = {Dependable Computing and Fault Tolerant Systems},
    BOOKTITLE = {Dependable Computing for Critical Applications---6},
    PUBLISHER = {{IEEE} Computer Society},
    EDITOR = {Mario Dal Cin and Catherine Meadows and William {H.} Sanders}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy