Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms
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.
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
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/}
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page