|
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 203222.
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
|
|