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

Formal Verification of Algorithms for Critical Systems
 by Dr. John Rushby & Friedrich von Henke.

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

Appears in IEEE Transactions on Software Engineering, Volume 19, Number 1.
January, 1993.
Pages 13–23.


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.

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/}
}
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