Issue No. 01 - January (1993 vol. 19)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.210304
<p>The authors describe their 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. The problems encountered in unsynchronized systems and the necessity, and criticality, of fault-tolerant synchronization are described. An overview of one such algorithm and of the arguments for its correctness are given. A verification of the algorithm performed using the authors' EHDM system for formal specification and verification is described. The errors found in the published analysis of the algorithm and benefits derived from the verification are indicated. Based on their experience, the authors derive some key requirements for a formal specification and verification system adequate to the task of verifying algorithms of the type considered. The conclusions regarding the benefits of formal verification in this domain and the capabilities required of verification systems in order to realize those benefits are summarized.</p>
critical systems; machine-checked verification; Byzantine fault-tolerant algorithm; digital flight control system; fault-tolerant synchronization; EHDM system; formal specification; fault tolerant computing; formal specification; formal verification; safety; software reliability; synchronisation
F. von Henke and J. Rushby, "Formal Verification of Algorithms for Critical Systems," in IEEE Transactions on Software Engineering, vol. 19, no. , pp. 13-23, 1993.