This Article 
 Bibliographic References 
 Add to: 
Formal Verification of Algorithms for Critical Systems
January 1993 (vol. 19 no. 1)
pp. 13-23

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.

[1] "Reprogramming capability proves key to extending Voyager 2's journey,"Aviation Week and Space Technology, Aug. 7, 1989, p. 72.
[2] J. Barwise, "Mathematical proofs of computer system correctness,"Notices of the AMS, vol. 36, pp. 844-851, Sept. 1989.
[3] M. J. Beeson, "Toward a computation system based on set theory,"Theoretical Computer Science, vol. 60, pp. 297-340, 1988.
[4] R. S. Boyer and J. S. Moore,A Computational Logic Handbook. Boston, MA: Academic, 1988.
[5] R. W. Butler, J. L. Caldwell, and B. L. Di Vito, "Design strategy for a formally verified reliable computing platform," inCOMPASS '91, Proc. 6th Annual Conf. on Computer Assurance, Gaithersburg, MD, June 1991, pp. 125-133.
[6] J. H. Cheng and C. B. Jones, "On the usability of logics which handle partial functions," in C. Morgan and J. C. P. Woodcock, Eds.,Proc. 3rd Refinement Workshop. New York: Springer-Verlag, 1990, pp. 51-69.
[7] Department of Defense Trusted Computer System Evaluation Criteria. Department of Defense, DOD 5200.28-STD (supersedes CSC-STD-001- 83), Dec. 1985.
[8] B. L. Di Vito, R. W. Butler, and J. L. Caldwell, "High level design proof of a reliable computing platform," in J. F. Meyer and R. D. Schlichting, Eds.,Dependable Computing for Critical Applications-2, vol. 6,Dependable Computing and Fault-Tolerant Systems. New York: Springer-Verlag, 1991, pp. 279-306.
[9] System Design Analysis, Federal Aviation Administration, Advisory Circular 25.1309-1, Sept. 7, 1982.
[10] J. R. Garman, "The 'bug' heard 'round the world,"ACM Software Eng. Notes, vol. 6, no. 5, pp. 3-10, Oct. 1981.
[11] R. E. Harper and J. H. Lala, "Fault-tolerant parallel processor,"AIAA J. Guidance, Contr., and Dynamics, vol. 14, no. 3, pp. 554-563, May-June 1991.
[12] I. Hayes, Ed.,Specification Case Studies (Series in Computer Science). Englewood Cliffs, NJ: Prentice-Hall International, 1987.
[13] R. M. Kieckhafer, C. J. Walter, A. M. Finn, and P. M. Thambidurai, "The MAFT architecture for distributed fault tolerance,"IEEE Trans. Comput., vol. 37, no. 4, pp. 398-405, Apr. 1988.
[14] I. Kleiner, "Rigor and proof in mathematics: A historical perspective,"Mathematics Mag., vol. 64, no. 5, pp. 291-314, Dec. 1991.
[15] H. Kopetzet al., "Distributed fault-tolerant real-time systems: The Mars approach,"IEEE Micro, vol. 9, no. 1, pp. 25-40, Feb. 1989.
[16] I. Lakatos,Proofs and Refutations. Cambridge, England: Cambridge University Press, 1976.
[17] L. Lamport and P.M. Melliar-Smith, "Synchronizing Clocks in the Presence of Faults,"J. ACM, Vol. 32, No. 1, Jan. 1985, pp. 52-78.
[18] L. Lamport, R. Shostak, and M. Pease, "The Byzantine Generals Problem,"ACM Trans. Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 382-401.
[19] D. A. Mackall, "AFTI/F-16 digital flight control system experience," in G. P. Beasley, ed.,NASA Aircraft Controls Research 1983, NASA Conference Publication 2296, 1984. Proceedings of workshop held at NASA Langley Research Center, Hampton, VA, Oct. 25-27, 1983, pp. 469-487.
[20] D. A. Mackall, "Development and flight test experiences with a flightcrucial digital control system," NASA Tech. Paper 2857, NASA Ames Research Center, Dryden Flight Research Facility, Edwards AFB, CA, 1988.
[21] S. Owre, J. M. Rushby, and N. Shankar, "PVS: A prototype verification system," in D. Kapur, Ed.,11th Int. Conf. on Automated Deduction (CADE), no. 607 in Lecture Notes in Artificial Intelligence, Saratoga, NY. New York: Springer-Verlag, 1992, pp. 748-752.
[22] M. Pease, R. Shostak, and L. Lamport, "Reaching agreement in the presence of faults,"J. Ass. Comput. Mach., vol. 27, pp. 228-234, Apr. 1980.
[23] D. Puyplat, "A320: First of the computer-age aircraft"Aerospace America, vol. 29, no. 5, pp. 28-30, May 1991.
[24] P. Ramanathan, K. G. Shin, and R. W. Butler, "Fault-tolerant clock synchronization in distributed systems,"IEEE Computer, vol. 23, no. 10, pp. 33-42, Oct. 1990.
[25] J. Rushby, "Formal specification and verification of a fault-masking and transient-recovery model for digital flight-control systems," in J. Vytopil, Ed.,Formal Techniques in Real-Time and Fault-Tolerant Systems, vol. 571,Lecture Notes in Computer Science. New York: Springer-Verlag, 1992, pp. 237-257.
[26] J. Rushby, "Formal verification of an Oral Messagaes algorithm for interactive consistency," Tech. Rep. SRI-CSL-92-1, Computer Science Laboratory, SRI International, Menlo Park, CA, June 1992.
[27] J. Rushby and F. von Henke, "Formal verification of the Interactive Convergence clock synchronization algorithm using EHDM," Tech. Rep. SRI-CSL-89-3R, Computer Science Laboratory, SRI International, Menlo Park, CA, Feb. 1989(revised Aug. 1991); original version also available as NASA Contractor Rep. 4239.
[28] J. Rushby, F. von Henke, and S. Owre, "An introduction to formal specification and verification using EHDM, Tech. Rep. SRI-CSL-91-2, Computer Science Laboratory, SRI International, Menlo Park, CA, Feb. 1991.
[29] F. B. Schneider, "Understanding protocols for byzantine clock synchronization," Cornell Univ. Tech. Rep. 87-859, Aug. 1987.
[30] N. Shankar, "Mechanical verification of a generalized protocol for Byzantine fault-tolerant clock synchronization," in J. Vytopil, Ed.,Formal Techniques in Real-Time and Fault-Tolerant Systems, vol. 571,Lecture Notes in Computer Science. New York: Springer-Verlag, pp. 217-236, 1992.
[31] R. E. Shostak, "A practical decision procedure for arithmetic with function symbols,"J. Ass. Comput. Mach., vol. 26, no. 2, pp. 351-360, Apr. 1979.
[32] J. M. Spivey,The Z Notation: A Reference Manual (Computer Science Series). Englewood Cliffs, NJ: Prentice Hall International, 1989.
[33] Interim Defence Standard 00-55: The procurement of safety critical software in defence equipment, Part 1, Issue 1: Requirements; Part 2, Issue 1: Guidance, U.K. Ministry of Defence, Apr. 1991.
[34] J. Vytopil, Ed.,Formal Techniques in Real-Time and Fault-Tolerant Systems, vol. 571,Lecture Notes in Computer Science. New York Springer-Verlag, 1992.
[35] J. H. Wensleyet al., "SIFT: Design and analysis of a fault-tolerant computer for aircraft control,"Proc. IEEE, vol. 66, no. 10, pp. 1240-1255, Oct. 1978.
[36] W. D. Young, "Verifying the interactive convergence clock-synchronization algorithm using the Boyer-Moore prover," NASA Contractor Rep. 189649, NASA Langley Research Center, Hampton, VA, Apr. 1992 (work performed by Computational Logic Inc.).

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
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, Jan. 1993, doi:10.1109/32.210304
Usage of this product signifies your acceptance of the Terms of Use.