This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS
February 1995 (vol. 21 no. 2)
pp. 107-125
PVS is the most recent in a series of verification systems developed at SRI. Its design was strongly influenced, and later refined, by our experiences in developing formal specifications and mechanically checked verifications for the fault-tolerant architecture, algorithms, and implementations of a model “reliable computing platform” (RCP) for life-critical digital flight-control applications, and by a collaborative project to formally verify the design of a commercial avionics processor called AAMP5. Several of the formal specifications and verifications performed in support of RCP and AAMP5 are individually of considerable complexity and difficulty. But in order to contribute to the overall goal, it has often been necessary to modify completed verifications to accommodate changed assumptions or requirements, and people other than the original developer have often needed to understand, review, build on, modify, or extract part of an intricate verification. In this paper, we outline the verifications performed, present the lessons learned, and describe some of the design decisions taken in PVS to better support these large, difficult, iterative, and collaborative verifications.

[1] Federal Aviation Administration,“System Design and Analysis,”Advisory Circular 25.1309-1A, June 21, 1988.
[2] R. W. Dennis and A. D. Hills,“A fault tolerant fly by wire system for maintenance free applications,”in9th AIAA/IEEE Digital Avionics Syst. Conf.Virginia Beach, VA, Oct. 1990, pp. 11–20.
[3] D. A. Mackall,“Development and flight test experiences with a flight-crucial digital control system,”NASA Tech. Paper 2857, NASA Ames Res. Ctr., Dryden Flight Res. Facility, Edwards, CA, 1988.
[4] J. H. Wensleyet al.,“SIFT: Design and analysis of a fault-tolerant computer for aircraft control,”inProc. IEEE,vol. 66, Oct. 1978, pp. 1240–1255.
[5] M. Pease, R. Shostak, and L. Lamport, “Reaching Agreement in the Presence of Faults,” J. ACM, vol. 27, no. 2, pp. 228–234, Apr. 1980.
[6] 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, pp. 398–405, Apr. 1988.
[7] P. Thambidurai and Y.-K. Park,“Interactive consistency with multiple failure modes,”inIEEE 7th Symp. Reliable Distribut. Syst.,Columbus, OH, Oct. 1988, pp. 93–100.
[8] P. M. Melliar-Smith and R. L. Schwartz,“Formal specification and verification of SIFT: A fault-tolerant flight control system,”IEEE Trans. Comput.,vol. C-31, pp. 616–630, July 1982.
[9] W. R. Bevier and W. D. Young,“Machine checked proofs of the design of a fault-tolerant circuit,”Formal Aspects of Computing,vol. 4, no. 6A, pp. 755–775, 1992.
[10] M. Srivas and M. Bickford,“Verification of the Ft.-Cayuga fault-tolerant microprocessor system, Vol. 1: A case-study in theorem prover-based verification,”NASA Langley Res. Ctr., Hampton, VA, Contractor Rep. 4381, July 1991.
[11] P. M. Melliar-Smith and J. Rushby,“The Enhanced HDM system for specification and verification,”inProc. VerkShop III,pp. 41–43, published asACM Software Engineering Notes, vol. 10, no. 4, Aug. 85.
[12] J. M. Spitzen, K. N. Levitt, and L. Robinson,“An example of hierarchical design and proof,”Commun. ACM,vol. 21, no. 12, pp. 1064–1075, Dec. 1978.
[13] R. E. Shostak,“Deciding combinations of theories,”J. ACM,vol. 31, no. 1, pp. 1–12, Jan. 1984.
[14] J. Rushby, F. von Henke, and S. Owre,“An introduction to formal specification and verification using EHDM ,”Computer Sci. Lab., SRI International, Menlo Park, CA, Tech. Rep. SRI-CSL-91-2, Feb. 1991.
[15] S. Owre, J.M. Rushby, and N. Shankar, "PVS: A Prototype Verification System," E. Kapur, ed., Proc. 11th Conf. Automated Deduction, Lecture Notes in Computer Science 607. Springer-Verlag, 1992.
[16] M. Gordon, R. Milner, and C. Wadsworth,“Edinburgh LCF: A mechanized logic of computation,”inLecture Notes in Computer Sci.New York: Springer-Verlag, vol. 78, 1979.
[17] N. Shankar, "Verification of Real-Time Systems Using PVS," Computer Aided Verification, CAV '93, Lecture Notes in Computer Science 697. Springer-Verlag, June-July 1993.
[18] J.U. Skakkebæk and N. Shankar, "Towards a Duration Calculus Proof Assistant in PVS," Formal Techniques in Real-time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863. Springer-Verlag, Sept. 1994.
[19] J. Hooman, "Correctness of Real Time Systems by Construction," Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, pp. 19-40. Springer-Verlag, Sept. 1994.
[20] L. Lamport and P.M. Melliar-Smith, “Synchronizing Clocks in the Presence of Faults,” J. ACM, vol. 32, no. 1, pp. 52–78, Jan. 1985.
[21] J. Rushby and F. von Henke,“Formal verification of the Interactive Convergence clock synchronization algorithm using EHDM,”Computer Sci. Lab., SRI International, Menlo Park, CA, Feb. 1989 (Rev. Aug. 1991); original version also available as NASA Contractor Rep. 4239, June 1989.
[22] ——,“Formal verification of algorithms for critical systems,”IEEE Trans. Software Eng.,vol. 19, pp. 13–23, Jan. 1993.
[23] W.D. Young, "Verifying the Interactive Convergence Clock Synchronization Algorithm Using the Boyer-Moore Theorem Prover," Contractor Report 189649, NASA, Apr. 1992.
[24] E. Liu and J. Rushby,“A formally verified module to support Byzantine fault-tolerant clock synchronization,”Computer Sci. Lab., SRI International, Menlo Park, CA, Project rep. 8200-130, Dec. 1993.
[25] D. L. Palumbo and R. Lynn Graham,“Experimental validation of clock synchronization algorithms,”NASA Langley Res. Ctr., Hampton, VA, NASA Tech. Paper 2857, July 1992.
[26] J. Rushby, “A Formally Verified Algorithm for Clock Synchronization under a Hybrid Fault Model,” Proc. 13th ACM Symp. Principles of Distributed Computing, pp. 304–313, Los Angeles, Calif., Aug. 1994. Also available as NASA Contractor Report 198289
[27] F.B. Schneider,"Understanding Protocols for Byzantine Clock Synchronization," Report No. 87-859, Dept. of Computer Science, Cornell Univ., Aug. 1987.
[28] N. Shankar, “Mechanical Verification of a Generalized Protocol for Byzantine Fault-Tolerant Clock Synchronization,” pp. 217-236, Jan. 1992.
[29] P. S. Miner,“Verification of fault-tolerant clock synchronization systems,”NASA Langley Res. Ctr., Hampton, VA, NASA Tech. Paper 3349, Nov. 1993.
[30] J. Lundelius Welch and N. Lynch, “A New Fault-Tolerant Algorithm for Clock Synchronization,” Information Computing 77, pp. 1-36, 1988.
[31] P. S. Miner, S. Pullela, and S. D. Johnson,“Interaction of formal design systems in the development of a fault-tolerant clock synchronization circuit,”inIEEE 13th Symp. Reliable Distribut. Syst.,Dana Point, CA, Oct. 1994, pp. 128–137.
[32] B. Bose,“DDD—a transformation system for Digital Design Deriviation,”Computer Sci. Dep., Indiana Univ., Bloomington, IN, Tech. Rep. 331, May 1991.
[33] 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.
[34] W. R. Bevier and W. D. Young,“Machine-checked proofs of a Byzantine agreement algorithm,”Computational Logic Inc., Austin, TX, Tech. Rep. 55, June 1990.
[35] J. Rushby, “Formal Verification of an Oral Messages Algorithm for Interactive Consistency,” Technical Report SRI-CSL-92-1, Computer Science Laboratory, SRI Int'l, Menlo Park, Calif., July 1992. also available as NASA Contractor Report 189704, Oct. 1992.
[36] P. Lincoln and J. Rushby, “Formal Verification of an Agorithm for Interactive Consistency Under a Hybrid Fault Model,” Proc. Computer-Aided Verification, CAV '93, pp. 292–304, C. Courcoubetis, ed., Elounda, Greece, Lecture Notes in Computer Science 697, Springer-Verlag, June/July 1993.
[37] ——,“A formally verified algorithm for interactive consistency under a hybrid fault model,”inIEEE Fault Tolerant Computing Symp. 23,Toulouse, France, June 1993, pp. 402–411.
[38] R. S. Boyer and J. S. Moore,“MJRTY—a fast majority vote algorithm,”inAutomated Reasoning: Essays in Honor of Woody Bledsoe,ofAutomated Reasoning Series,R. S. Boyer, Ed. Dordrecht, The Netherlands: Kluwer, vol. 1, pp. 105–117, 1991.
[39] P. Lincoln and J. Rushby,“Formal verification of an algorithm for interactive consistency under a hybrid fault model,”Computer Sci. Lab., SRI International, Menlo Park, CA, Tech. Rep. SRI-CSL-93-2, Mar. 1993; also available as NASA Contractor Rep. 4527, July 1993.
[40] A. L. Hopkins, Jr., J. H. Lala, and T. B. Smith III,“The evolution of fault tolerant computing at the Charles Stark Draper Laboratory, 1955–85,”inThe Evolution of Fault-Tolerant Computing,vol. 1 ofDependable Computing and Fault-Tolerant Systems,A. Aviienis, H. Kopetz, and J. C. Laprie, Eds. Vienna, Austria: Springer-Verlag, 1987, pp. 121–140.
[41] J. H. Lala,“A Byzantine resilient fault tolerant computer for nuclear power application,”inIEEE Fault Tolerant Computing Symp. 16,Vienna, Austria, July 1986, pp. 338–343.
[42] P. Lincoln and J. Rushby,“Formal verification of an interactive consistency algorithm for the Draper FTP architecture under a hybrid fault model,”inIEEE COMPASS '94 (Proc. 9th Annual Conf. Comput. Assurance),Gaithersburg, MD, June 1994, , pp. 107–120.
[43] B. L. Di Vito, R. W. Butler, and J. L. Caldwell,“High level design proof of a reliable computing platform,”in Meyer and Schlichting [83], pp. 279–306.
[44] J. Rushby,“A fault-masking and transient-recovery model for digital flight-control systems,”inFormal Techniques in Real-Time and Fault-Tolerant Systems,J. Vytopil, Ed. Norwell, MA: Kluwer, ch. 5, pp. 109–136, 1993.
[45] R. W. Butler, B. L. Di Vito, and C. M. Holloway,“Formal design and verification of a reliable computing platform for real-time control: Phase 3 results,”NASA Langley Res. Ctr., Hampton, VA, NASA Tech. Memo. 109140, Aug. 1994.
[46] B. L. Di Vito and R. W. Butler,“Formal techniques for synchronized fault-tolerant systems,”inDependable Computing for Critical Applications—3,inDependable Computing and Fault-Tolerant Systems.C. E. Landwehr, B. Randell, and L. Simoncini, Eds. Vienna, Austria: Springer-Verlag, vol. 8, pp. 163–188, Sept. 1992.
[47] S. P. Miller and M. Srivas,“Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods,”to be presented atWIFT'95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL, Apr. 5–8, 1995.
[48] D. W. Best, C. E. Kress, N. M. Mykris, J. D. Russell, and W. J. Smith,“An advanced-architecture CMOS/SOS microprocessor,”IEEE Micro,vol. 2, pp. 11–26, Aug. 1982.
[49] W. C. Carter, W. H. Joyner, Jr., and D. Brand,“Microprogram verification considered necessary,”inNat. Comput. Conf., AFIPS Conf. Proc.,1978, vol. 48, pp. 657–664.
[50] J. V. Cook,“Verification of the C/30 microcode using the State Delta Verification System (SDVS),”inProc. 13th Nat. Comput. Security Conf.,Washington, DC, Oct. 1990, pp. 20–31.
[51] D. May, G. Barrett, and D. Shepherd,“Designing chips that work,”in Hoare and Gordon [84], pp. 3–19.
[52] W. A. Hunt, Jr.,FM8501: A Verified Microprocessor, vol. 795 ofLecture Notes in Artificial Intelligence.Berlin: Springer-Verlag, 1994.
[53] W. A. Hunt, Jr. and B. C. Brock,“A formal HDL and its use in the FM9001 verification,”in Hoare and Gordon [84] , pp. 35–47.
[54] J. Rushby,“Formal methods and digital systems validation for airborne systems,”Computer Sci. Lab., SRI International, Menlo Park, CA, Tech. Rep. SRI-CSL-93-7, Dec. 1993; also available as NASA Contractor Rep. 4551, Dec. 1993.
[55] R. R. Lutz,“Analyzing software requirements errors in safety-critical embedded systems,”inIEEE Int. Symp. Requirements Eng.,San Diego, CA, Jan. 1993, pp. 126–133.
[56] J. Guttag and J. J. Horning,“Formal specification as a design tool,”in7th ACM Symp. on Principles of Programming Languages,Las Vegas, NV, Jan. 1980, pp. 251–261.
[57] N. Shankar,“Abstract datatypes in PVS,”Computer Sci. Lab., SRI International, Menlo Park, CA, Tech. Rep. SRI-CSL-93-9, Dec. 1993.
[58] J. H. Cheng and C. B. Jones,“On the usability of logics which handle partial functions,”inProc 3rd Refinement Workshop,inSpringer-Verlag Workshops in Computing.C. Morgan and J. C. P. Woodcock, Eds., 1990, pp. 51–69.
[59] J. R. Shoenfield,Mathematical Logic.Reading, MA: Addison-Wesley, 1967.
[60] J. Ousterhout, Tcl and the Tk Toolkit, Addison Wesley Longman, Reading, Mass., 1994.
[61] I. Lakatos,Proofs and Refutations.Cambridge, England: Cambridge University Press, 1976.
[62] I. Kleiner,“Rigor and proof in mathematics: A historical perspective,”inMathematics Magazine, vol. 64, no. 5, pp. 291–314, Dec. 1991.
[63] R. E. Shostak,“On the SUP-INF method for proving Presburger formulas,”J. ACM,vol. 24, no. 4, pp. 529–543, Oct. 1977.
[64] ——,“Deciding linear inequalities by computing loop residues,”J. ACM,vol. 28, no. 4, pp. 769–779, Oct. 1981.
[65] R. S. Boyer and J. S. Moore,“Integrating decision procedures into heuristic theorem provers: A case study with linear arithmetic,”inMachine Intelligence,vol. 11. London: Oxford University Press, 1986.
[66] M.-J.-C. Gordon and T.-F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. ISBN 0-521-44189-7. Cambridge Univ. Press, 1993.
[67] G. L. J. M. Janssen,ROBDD Software,Dep. of Elec. Eng., Eindhoven Univ. of Technology, Oct. 1993.
[68] D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas,“Effective theorem proving for hardware verification,”inPreliminary Proc. 2nd Conf. Theorem Provers in Circuit Design.(Germany: Bad Herrenalb), Sept. 1994, pp. 287–305.
[69] R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[70] F. K. Hanna, N. Daeche, and M. Longley,“Specification and verification using dependent types,”IEEE Trans. Software Eng.,vol. 16, pp. 949–964, Sept. 1989.
[71] T. Yuasa and R. Nakajima,“IOTA: A modular programming system,”IEEE Trans. Software Eng.,vol. SE-11, pp. 179–187, Feb. 1985.
[72] R. S. Boyer and J. S. Moore,A Computational Logic.New York: Academic, 1979.
[73] R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
[74] R. Melton and D. L. Dill,Mur$\phi$Annotated Reference Manual.Stanford, CA: Computer Sci. Dep., Stanford Univ., Mar. 1993.
[75] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[76] J.R. Burch and D.L. Dill, "Automatic Verification of Pipelined Microprocessor Control," Proc. Computer-Aided Verification (CAV 94), Springer-Verlag, 1994, pp. 68-80.
[77] D. Cyrluk and P. Narendran,“Ground temporal logic—a logic for hardware verification,”inComputer-Aided Verification, CAV '94,vol. 818 ofLecture Notes in Computer Science,D. Dill, Ed. New York: Springer-Verlag, pp. 247–259.
[78] K. L. Heninger,“Specifying software requirements for complex systems: New techniques and their application,”IEEE Trans. Software Eng.,vol. SE-6, pp. 2–13, Jan. 1980.
[79] J. Rushby and M. Srivas,“Using PVS to prove some theorems of David Parnas,”inHigher Order Logic Theorem Proving and its Applications (6th Int. Workshop, HUG '93),no. 780 inLecture Notes in Computer Science,J. J. Joyce and C.-J. H. Seger, Eds. New York: Springer-Verlag, pp. 163–173.
[80] C. Courcoubetis ed., Proc. Fifth Int'l Conf. Computer Aided Verification,Elounda, Greece, 1993.
[81] H. Langmaack, W.-P. de Roever, and J. Vytopil, Eds.,Formal Techniques in Real-Time and Fault-Tolerant Systems,vol. 863 ofLecture Notes in Computer Science.New York: Springer-Verlag, Sept. 1994.
[82] J. Vytopil, Ed.,Formal Techniques in Real-Time and Fault-Tolerant Systems,vol. 571 ofLecture Notes in Computer Science. New York: Springer-Verlag, Jan. 1992.
[83] J. F. Meyer and R. D. Schlichting, Eds.,Dependable Computing for Critical Applications—2,vol. 6 ofDependable Computing and Fault-Tolerant Systems.Vienna, Austria: Springer-Verlag, Feb. 1991.
[84] C. A. R. Hoare and M. J. C. Gordon, Eds.,Mechanized Reasoning and Hardware Design.Prentice Hall International Series in Computer Science, Hemel Hempstead, UK, 1992.

Index Terms:
Byzantine agreement, clock synchronization, fault tolerance, flight control, formal methods, formal specification, hardware verification, theorem proving, verification systems, PVS
Citation:
Sam Owre, John Rushby, Natarajan Shankar, Friedrich von Henke, "Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS," IEEE Transactions on Software Engineering, vol. 21, no. 2, pp. 107-125, Feb. 1995, doi:10.1109/32.345827
Usage of this product signifies your acceptance of the Terms of Use.