
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Sam Owre, John Rushby, Natarajan Shankar, Friedrich von Henke, "Formal Verification for FaultTolerant Architectures: Prolegomena to the Design of PVS," IEEE Transactions on Software Engineering, vol. 21, no. 2, pp. 107125, February, 1995.  
BibTex  x  
@article{ 10.1109/32.345827, author = {Sam Owre and John Rushby and Natarajan Shankar and Friedrich von Henke}, title = {Formal Verification for FaultTolerant Architectures: Prolegomena to the Design of PVS}, journal ={IEEE Transactions on Software Engineering}, volume = {21}, number = {2}, issn = {00985589}, year = {1995}, pages = {107125}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.345827}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Formal Verification for FaultTolerant Architectures: Prolegomena to the Design of PVS IS  2 SN  00985589 SP107 EP125 EPD  107125 A1  Sam Owre, A1  John Rushby, A1  Natarajan Shankar, A1  Friedrich von Henke, PY  1995 KW  Byzantine agreement KW  clock synchronization KW  fault tolerance KW  flight control KW  formal methods KW  formal specification KW  hardware verification KW  theorem proving KW  verification systems KW  PVS VL  21 JA  IEEE Transactions on Software Engineering ER   
[1] Federal Aviation Administration,“System Design and Analysis,”Advisory Circular 25.13091A, 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 flightcrucial 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 faulttolerant 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. MelliarSmith and R. L. Schwartz,“Formal specification and verification of SIFT: A faulttolerant flight control system,”IEEE Trans. Comput.,vol. C31, pp. 616–630, July 1982.
[9] W. R. Bevier and W. D. Young,“Machine checked proofs of the design of a faulttolerant circuit,”Formal Aspects of Computing,vol. 4, no. 6A, pp. 755–775, 1992.
[10] M. Srivas and M. Bickford,“Verification of the Ft.Cayuga faulttolerant microprocessor system, Vol. 1: A casestudy in theorem proverbased verification,”NASA Langley Res. Ctr., Hampton, VA, Contractor Rep. 4381, July 1991.
[11] P. M. MelliarSmith 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. SRICSL912, 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. SpringerVerlag, 1992.
[16] M. Gordon, R. Milner, and C. Wadsworth,“Edinburgh LCF: A mechanized logic of computation,”inLecture Notes in Computer Sci.New York: SpringerVerlag, vol. 78, 1979.
[17] N. Shankar, "Verification of RealTime Systems Using PVS," Computer Aided Verification, CAV '93, Lecture Notes in Computer Science 697. SpringerVerlag, JuneJuly 1993.
[18] J.U. Skakkebæk and N. Shankar, "Towards a Duration Calculus Proof Assistant in PVS," Formal Techniques in Realtime and FaultTolerant Systems, Lecture Notes in Computer Science 863. SpringerVerlag, Sept. 1994.
[19] J. Hooman, "Correctness of Real Time Systems by Construction," Formal Techniques in RealTime and FaultTolerant Systems, Lecture Notes in Computer Science 863, pp. 1940. SpringerVerlag, Sept. 1994.
[20] L. Lamport and P.M. MelliarSmith, “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 BoyerMoore Theorem Prover," Contractor Report 189649, NASA, Apr. 1992.
[24] E. Liu and J. Rushby,“A formally verified module to support Byzantine faulttolerant clock synchronization,”Computer Sci. Lab., SRI International, Menlo Park, CA, Project rep. 8200130, 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. 87859, Dept. of Computer Science, Cornell Univ., Aug. 1987.
[28] N. Shankar, “Mechanical Verification of a Generalized Protocol for Byzantine FaultTolerant Clock Synchronization,” pp. 217236, Jan. 1992.
[29] P. S. Miner,“Verification of faulttolerant clock synchronization systems,”NASA Langley Res. Ctr., Hampton, VA, NASA Tech. Paper 3349, Nov. 1993.
[30] J. Lundelius Welch and N. Lynch, “A New FaultTolerant Algorithm for Clock Synchronization,” Information Computing 77, pp. 136, 1988.
[31] P. S. Miner, S. Pullela, and S. D. Johnson,“Interaction of formal design systems in the development of a faulttolerant 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. 382401.
[34] W. R. Bevier and W. D. Young,“Machinechecked 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 SRICSL921, 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. ComputerAided Verification, CAV '93, pp. 292–304, C. Courcoubetis, ed., Elounda, Greece, Lecture Notes in Computer Science 697, SpringerVerlag, 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. SRICSL932, 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 FaultTolerant Computing,vol. 1 ofDependable Computing and FaultTolerant Systems,A. Aviienis, H. Kopetz, and J. C. Laprie, Eds. Vienna, Austria: SpringerVerlag, 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 faultmasking and transientrecovery model for digital flightcontrol systems,”inFormal Techniques in RealTime and FaultTolerant 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 realtime 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 faulttolerant systems,”inDependable Computing for Critical Applications—3,inDependable Computing and FaultTolerant Systems.C. E. Landwehr, B. Randell, and L. Simoncini, Eds. Vienna, Austria: SpringerVerlag, 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 IndustrialStrength 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 advancedarchitecture 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: SpringerVerlag, 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. SRICSL937, Dec. 1993; also available as NASA Contractor Rep. 4551, Dec. 1993.
[55] R. R. Lutz,“Analyzing software requirements errors in safetycritical 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. SRICSL939, Dec. 1993.
[58] J. H. Cheng and C. B. Jones,“On the usability of logics which handle partial functions,”inProc 3rd Refinement Workshop,inSpringerVerlag Workshops in Computing.C. Morgan and J. C. P. Woodcock, Eds., 1990, pp. 51–69.
[59] J. R. Shoenfield,Mathematical Logic.Reading, MA: AddisonWesley, 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 SUPINF 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 0521441897. 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. SE11, 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. ComputerAided Verification (CAV 94), SpringerVerlag, 1994, pp. 6880.
[77] D. Cyrluk and P. Narendran,“Ground temporal logic—a logic for hardware verification,”inComputerAided Verification, CAV '94,vol. 818 ofLecture Notes in Computer Science,D. Dill, Ed. New York: SpringerVerlag, pp. 247–259.
[78] K. L. Heninger,“Specifying software requirements for complex systems: New techniques and their application,”IEEE Trans. Software Eng.,vol. SE6, 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: SpringerVerlag, 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 RealTime and FaultTolerant Systems,vol. 863 ofLecture Notes in Computer Science.New York: SpringerVerlag, Sept. 1994.
[82] J. Vytopil, Ed.,Formal Techniques in RealTime and FaultTolerant Systems,vol. 571 ofLecture Notes in Computer Science. New York: SpringerVerlag, Jan. 1992.
[83] J. F. Meyer and R. D. Schlichting, Eds.,Dependable Computing for Critical Applications—2,vol. 6 ofDependable Computing and FaultTolerant Systems.Vienna, Austria: SpringerVerlag, 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.