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 (1999)
 by Dr. John Rushby.

Appears in IEEE Transactions on Software Engineering, Volume 25, Number 5.
September, 1999.
Pages 651–660.


Abstract
Many critical real-time applications are implemented as time-triggered systems. We present a systematic way to derive such time-triggered implementations from algorithms specified as functional programs (in which form their correctness and fault-tolerance properties can be formally and mechanically verified with relative ease). The functional program is first transformed into an untimed synchronous system, and then to its time-triggered implementation. The first step is specific to the algorithm concerned, but the second is generic and we prove its correctness. This proof has been formalized and mechanically checked with the PVS verification system. The approach provides a methodology that can ease the formal specification and assurance of critical fault-tolerant systems.
BibTEX Entry
@article{Rushby99:TSE,
    AUTHOR = {John Rushby},
    TITLE = {Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms},
    JOURNAL = {{IEEE} Transactions on Software Engineering},
    VOLUME = {25},
    NUMBER = {5},
    YEAR = {1999},
    PAGES = {651--660},
    MONTH = {sep},
    URL = {http://www.csl.sri.com/papers/tse99/}
}
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