The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.01 - January (1993 vol.19)
pp: 13-23
ABSTRACT
<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>
INDEX TERMS
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
CITATION
J.M. Rushby, F. von Henke, "Formal Verification of Algorithms for Critical Systems", IEEE Transactions on Software Engineering, vol.19, no. 1, pp. 13-23, January 1993, doi:10.1109/32.210304
21 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool