This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Application of Formal Analysis to Software in a Fault-Tolerant Environment
October 1999 (vol. 48 no. 10)
pp. 1053-1064

Abstract—This paper describes work that represents the culmination of a comprehensive hardware/software modeling and analysis project concerning the Charles Stark Draper Laboratory Fault-Tolerant Processor (FTP). The FTP performs a safety-related function at the Integral Fast Reactor (IFR previously known as the Experimental Breeder Reactor-II) operated by Argonne National Laboratory for the Department of Energy. Previously, we demonstrated the tolerance to hardware failures of data exchange instructions on the FTP. Here, we describe a methodology for assuring that the software executing on the FTP is also tolerant to hardware failures. This methodology is based on an abstraction of the program data and control flows in terms of the specification of an abstract application program that operates on the FTP. We then prove the fault tolerance of the abstract application program to hardware and sensor failures. Based on a more detailed specification and analysis of the code that is used in the application software, we demonstrate that this code satisfies the sufficient conditions developed for the abstract application program to claim system fault tolerance.

[1] G.H. Chisholm, J. Kljaich, B.T. Smith, and A.S. Wojcik, “An Approach to the Verification of a Fault-Tolerant, Computer-Based Reactor Safety System: A Case Study Using Automated Reasoning,” Interim Report NP-4924, Electric Power Research Inst., Palo Alto, Calif., 1987.
[2] A.J. Kljaich, A.B.T. Smith, and A.S. Wojcik, “Formal Verification of Fault Tolerance Using Theorem-Proving Techniques,” IEEE Trans. Computers, vol. 38, pp. 366-376, 1989.
[3] W.W. McCune, “OTTER 3.0 Reference Manual and Guide,” Technical Report ANL-90/9, Argonne Nat'l Laboratory, Mar. 1994.
[4] E.L. Lusk and R.A. Overbeek, “An LMA-Based Theorem Prover,” Technical Report ANL-82-84, Argonne Nat'l Laboratory, Dec. 1984.
[5] J. Kljaich, “Formal Verification of Digital Systems,” PhD dissertation, Dept. of Computer Science, Illinois Inst. of Technology, Chicago, Dec. 1985.
[6] A.S. Wojcik, J. Kljaich, and N. Srinivas, “A Formal Design Verification System Based on an Automated Reasoning System,” Proc. 21st Design Automation Conf., pp. 641-645, 1984.
[7] A.S. Wojcik, “Formal Design Verification of Digital Systems,” Proc. 20th Design Automation Conf., pp. 228-234, 1983.
[8] C.B. Jones, Systematic Software Development Using VDM.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[9] B. Potter, An Introduction to Formal Specification and Z. Englewood Cliffs, N.J.: Prentice Hall, 1991.
[10] D.A. Watt, Programming Language Concepts and Paradigms. New York: Prentice Hall, 1990.
[11] J.H. Wensley, “SIFT: Design and Analysis of a Fault-Tolerant Computer for Aircraft Control,” Proc. IEEE, vol. 66, pp. 1,240-1,255, 1988.
[12] J. Rushby and F. von Henke, "Formal Verification of Algorithms for Critical Systems," IEEE Trans. Software Engineering, vol. 19, no. 1, pp. 13-23, Jan. 1993.
[13] R. Boyer and J. Moore, “Proof Checking the RSA Public Key Encryption Algorithm,” Am. Math. Monthly, vol. 91, pp. 13-23, 1984.
[14] M. Abadi and L. Lamport, “Conjoining Specifications,” technical report, Digital Equipment Corporation, 1993.
[15] B. Alpern and F.B. Schneider, “Defining Liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181-185, 1985.
[16] G.W. Dinolt, L.A. Benzinger, and M.G. Yatabe, “Combining Components and Policies,” Proc. Computer Security Foundations Workshop VII, 1994.
[17] T. Fine, “A Framework for Composition,” Proc. 11th Ann. Conf. Computer Assurance, 1996.
[18] J. McLean, "The specification and modeling of computer security," Computer, vol. 23, no. 1, pp. 9-16, 1990.
[19] J. McLean, "A general theory of composition for trace sets closed under selective interleaving functions," Proc. 1994 IEEE Symp. Research in Security and Privacy. IEEE Press, 1994.
[20] See, e.g., J.K. Millen, "Security Kernel Validation in Practice," Comm. ACM, vol. 19, pp. 244-250, 1976.
[21] R.M. Needham, “Authentication,” Safe and Secure Computing Systems, T. Anderson, ed., pp. 189-196, Blackwell Scientific Publications, 1989.
[22] P.G. Neumann, “On Hierarchical Design of Computer Systems for Critical Applications,” IEEE Trans. Software Eng., vol. 12, pp. 905-920, 1986.
[23] J.M. Rushby, “Design and Verification of Secure Systems,” Operating Systems Review, vol. 15, pp. 12-21, 1981.
[24] J. Rushby, “Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control System,” Computer Science Laboratory Report SRI-CSL-91-03, SRI Int'l, June 1991.
[25] D. Denning,"A lattice model of secure information flow," Comm. ACM, vol. 19, no. 5, pp. 236-243, 1976.
[26] D.E. Denning, “Secure Databases and Safety: Some Unexpected Conflicts,” Safe and Secure Computing Systems, T. Anderson, ed., pp. 101-111, Blackwell Scientific Publications, 1989.
[27] B. Auernheimer and R.A. Kemmerer, “ASLAN User's Manual,” technical report, Dept. of Computer Science, Univ. of California, Santa Barbara, Aug. 1984.
[28] L.K. Dillon, “Verifying General Safety Properties of Ada Tasking Programs,” IEEE Trans. Software Eng., vol. 16, pp. 51-63, 1990.
[29] D.L. Parnas, A.J. v. Schouwen, and S.P. Kwan, “Evaluation Standards for Safety Critical Software,” Technical Report 88-220, Dept. of Computing and Information Science, Queen's Univ. at Kingston, 1988.
[30] N.G. Leveson, “Safety-Critical Software Development,” Safe and Secure Computing Systems, T. Anderson, ed., pp. 155-162, Blackwell Scientific Publications, 1989.
[31] D.L. Parnas, A.J. van Schouwen, and S.P. Kwan, "Evaluation of safety-critical software," Comm. ACM, vol. 33, no.6, pp. 636-648, June 1990.
[32] J. Bengt, “Compositional Specification and Verification of Distributed Systems,” ACM Trans. Programming Languages and Systems, vol. 16, no. 2, pp. 259-303, Mar. 1994.
[33] IEEE, “Criteria for Protection of Systems for Nuclear Power Generating Stations,” Inst. of Electrical and Electronic Engineers, IEEE Standard IEEE 279-1971, 1971.
[34] IEEE and ANS, “Application Criteria for Programmable Digital Computer Systems in Safety Systems of Nuclear Power Generating Stations,” Inst. of Electrical and Electronic Engineers and Am. Nuclear Soc., IEEE/ANS Standard ANSI/IEEE-ANS-7.4.3.2, 1982.
[35] MoD, “Requirements for the Analysis of Safety Critical Hazards,” Ministry of Defence, Glasgow, Interim Defence Standard 00-56, May 1989.
[36] MoD, “Requirements for the Procurement of Safety Critical Software in Defence Equipment,” Ministry of Defence, Glasgow, Interim Defence Standard 00-55, May 1989.
[37] E. Jonsson and T. Olovsson, “On the Integration of Security and Dependability in Computer Systems,” Proc. IASTED Int'l Conf. Reliability, Quality Control and Risk Assessment, 1992.
[38] G.H. Chisholm and R.B. Jones, “Toward a Methodology for Formal Modeling of Battle Management Software,” technical memo, Argonne Nat'l Laboratory, 1993.
[39] V. Winter, G.H. Chisholm, B.T. Smith, and A.S. Wojcik, “A Formal Model for Verification of Abstract Properties,” Technical Report ANL-92/10, Argonne Nat'l Laboratory, Apr. 1992.
[40] J.H. Lala, R.E. Harper, and L.S. Alger, “A Design Approach for Ultrareliable Real-Time Systems,” Computer, vol. 24, pp. 12-22, 1991.
[41] ——,“The notion of proof in hardware verification,”J. Automated Reasoning, vol. 5, pp. 127–139, 1989.
[42] T. Suzuki, S. Shatz, and T. Murata, “A Protocol Modeling and Verification Approach Based on a Specification Language and Petri Nets,” IEEE Trans. Software Eng., vol. 16, pp. 523-536, 1990.
[43] “Special Issue on Formal Methods in Software Engineering,” IEEE Trans. Software Eng., 1990.
[44] B.L.D. Vito, R.W. Butler, and J.L. Caldwell, “Formal Design and Verification of a Reliable Computing Platform for Real-Time Control,” Technical Memorandum 102716, NASA Langley Research Center, Oct. 1990.
[45] Y.A. Papelis and T.L. Casavant, “Specification of Parallel/Distributed Software and Systems by Petri Nets with Transition Enabling Functions,” IEEE Trans. Software Eng., vol. 18, no. 3, Mar. 1992.
[46] D. Craigen, S. Gerhart, and T. Ralston, “An International Survey of Industrial Applications of Formal Methods,” Technical Report PB93-178564/AS, National Technical Information Service, Springfield, Va., 1993.
[47] H. Hempstead, Application of Formal Methods. U.K.: Prentice Hall, 1995.
[48] E.M. Clarke and R.P. Kurshan, "Computer-Aided Verification," IEEE Spectrum, pp. 61-67, June 1996.
[49] H.J. Genrich and K. Lautenbach, "System Modeling with High-Level Petri Nets," TCS 13, pp. 109-136, 1981. Also in [26].
[50] L. Wos et al., Automated Reasoning: Introduction and Applications, Prentice Hall, Upper Saddle River, N.J., 1984.
[51] Z. Manna,Mathematical theory of computation,New York: MacGraw Hill, 1974.
[52] J.M. Boyle and M.N. Muralidharan, “Program Reusability Through Program Transformation,” IEEE Trans. Software Eng., vol. 10, pp. 574-588, 1984.

Index Terms:
Formal analysis methodology, modeling and analysis of software and hardware, automated reasoning, fault tolerance.
Citation:
G.h. Chisholm, A.s. Wojcik, "An Application of Formal Analysis to Software in a Fault-Tolerant Environment," IEEE Transactions on Computers, vol. 48, no. 10, pp. 1053-1064, Oct. 1999, doi:10.1109/12.805155
Usage of this product signifies your acceptance of the Terms of Use.