Formal Verification of Algorithms for Critical Systems
John Rushby and Friedrich von Henke
Appears in IEEE Transactions on Software Engineering, Volume 19,
Number 1, January, 1993, pages 13-23.
A preliminary version of this paper was presented at SIGSOFT '91:
Software for Critical Systems, December 4-6, New Orleans, LA
(proceedings published as ACM SIGSOFT Engineering Notes, Volume 16,
Number 5, pp. 1-15).
Abstract
We describe our experience with formal, machine-checked verification
of algorithms for critical applications, concentrating on a Byzantine
fault-tolerant algorithm for synchronizing the clocks in the
replicated computers of a digital flight control system. First, we
explain the problems encountered in unsynchronized systems and the
necessity, and criticality, of fault-tolerant synchronization. We give
an overview of one such algorithm, and of the arguments for its
correctness. Next, we describe a verification of the algorithm that we
performed using our Ehdm system for formal specification and
verification. We indicate the errors we found in the published
analysis of the algorithm, and other benefits that we derived from the
verification. Based on our experience, we derive some key requirements
for a formal specification and verification system adequate to the
task of verifying algorithms of the type considered. Finally, we
summarize our conclusions regarding the benefits of formal
verification in this domain, and the capabilities required of
verification systems in order to realize those benefits.
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
BibTeX Entry
@article{Rushby&vonHenke93,
AUTHOR = {John Rushby and Friedrich von Henke},
TITLE = {Formal Verification of Algorithms for Critical Systems},
JOURNAL = {{IEEE} Transactions on Software Engineering},
VOLUME = {19},
NUMBER = {1},
YEAR = {1993},
PAGES = {13--23},
MONTH = {jan},
URL = {http://www.csl.sri.com/papers/tse93/}
}
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