This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Verification of Fault Tolerance Using Theorem-Proving Techniques
March 1989 (vol. 38 no. 3)
pp. 366-376
A formal verification system based on the use of automated reasoning techniques is described to validate fault tolerance. An extended Petri net representation, called a flow net, is described together with the theorem-proving implementation of a rule-based system for manipulating system descriptions. Examples taken from the literature are used to illustrate the representation and the capabiliti

[1] T. Higashino, M. Mori, Y. Sugiyama, K. Taniguchi, and T. Kasami, "An algebraic specification of HDLC procedures and its verification,"IEEE Trans. Software Eng., vol. SE-10, pp. 825-836, Nov. 1984.
[2] C. J. Kooman, "Algebraic specification and verification of communication protocols,"Sci. Comput. Programming, vol. 5, pp. 1-36, Feb. 1985.
[3] Barrow, H.G., "Verify: A Program for Proving Correctness of Digital Hardware Designs,"Artificial Intelligence, Vol. 24, 1984, pp. 437-491.
[4] J.A. Darringer, "The Application of Program Verification Techniques to Hardware Verification,"Proc. ACM IEEE 16th Design Automation Conf., June 1979, pp. 375-381.
[5] M. Gordon, "A model of register transfer systems with applications to microcode and VLSI correctness," Dep. Comput. Sci. Int. Rep. CSR- 82-81, Univ. of Edinburgh, Edinburgh, England, 1981.
[6] L. Haynes, "Logic design verification using static analysis," Ph.D. dissertation, Dep. Elec. Eng., Univ. Illinois, Urbana-Champaign, IL, May 1983.
[7] M. Monachino, "Design verification system for large scale LSI designs,"IBM J. Res. Develop., vol. 26, pp. 89-99, Jan 1982.
[8] V. Pitchumani and E. P. Stabler, "An inductive assertion method for register transfer level design verification,"IEEE Trans. Comput., vol. C-32, pp. 1073-1080, Dec. 1983.
[9] T. J. Wagner, "Hardware verification," Ph.D. dissertation, STAN-CS-77-632, Stanford Univ., 1977.
[10] A. Wojcik, "Formal Design Verification of Digital Systems,"Proc. Design Automation Conf., 1983, pp. 246-252.
[11] Wojcik, A.S., "A Formal Design Verification System Based on an Automated Reasoning System,"ACM IEEE 21st Design Automation Conf., July 1984, pp. 641-647.
[12] K. R. Apt, "Ten years of Hoare's-logic: A survey--Part one,"ACM Trans. Program. Lang. Syst., vol. 3, pp. 431-483, 1981.
[13] B. Elspas, K. N. Levitt, R. J. Waldinger, and A. Waksman, "An assessment of techniques for proving program correctness,"Comput. Surveys, vol. 4, pp. 97-147, June 1972.
[14] J. C. King, "Symbolic execution and program testing,"Commun. ACM, vol. 19, no. 7, pp. 385-394, 1976.
[15] M. H. Cheheyl, M. Gasser, G. A. Huff, and J. K. Millen, "Verifying security,"ACM Comput. Surveys, vol. 13, pp. 279-339, Sept. 1981.
[16] C.E. Landwehr, "Formal Models of Computer Security,"ACM Computer Surveys SIGOPS, Sept. 1981, pp. 247-278.
[17] T. B. Smith, "Fault tolerant processor concepts and operation," inProc. 14th Annu. Int. Conf. Fault-Tolerant Comput., Kissimmee, FL, June 1984, pp. 158-163.
[18] E. L. Lusk and R. A. Overbeek, "An LMA-based theorem prover," Math. and Comput. Sci. Div. Rep., Argonne Nat. Lab., Argonne, IL, Nov. 1982.
[19] E. L. Lusk and R. A. Overbeek, "The automated reasoning system ITP," Math. and Comput. Sci. Div. Rep., Argonne Nat. Lab., Argonne, IL 1984.
[20] E. L. Lusk, W. W. McCune, and R. A. Overbeek, "Logic machine architecture: Kernal functions," Math and Comput. Sci. Division Rep., Argonne Nat. Lab., Argonne, IL, Nov. 1982.
[21] T. McWilliams, "Verification of Timing Constraints on Large Digital Systems,"Proc. Design Automation Conf., 1980, pp. 139-147.
[22] A. E. Ruehli and G. S. Ditlow, "Circuit analysis, logic simulation, and design verification for VLSI,"Proc. IEEE, vol. 71, pp. 34-48, Jan. 1983.
[23] P. J. DesMarais, E. S. Y. Shew, and P. S. Wilcox, "A functional level modelling language for digital simulation," inProc. 19th Design Automat. Conf., Las Vegas, NV, June 1982, pp. 315-320.
[24] M. H. Doshi, R. B. Sullivan, and D. M. Schuler, "THEMIS logic simulator-A mix mode, multilevel, hiearchica., interactive digital circuit simulator," inProc. 21st Design Automat. Conf., Albuquerque, NM, June 1984, pp. 24-31.
[25] D. D. Hill and W. M. Van Cleemput, "SABLE: Multilevel simulator for hierarchical design," inProc. IEEE Int. Symp. Circuits Syst., Houston, TX, Apr. 1980, pp. 431-434.
[26] 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 utilizing automated reasoning," Elec. Power Res. Instit. Tech. Rep., Electric Power Res. Instit., Palo Alto, CA, 1986.
[27] D. L. Parnas, "Software aspects of strategic defense systems,"Amer. Scientist, vol. 73, pp. 432-440, Sept.-Oct. 1985.
[28] M. G. Genesereth, "Diagnosis using hierarchical design models," inProc. 1982 Nat. Conf. Artif. Intell. AAAI-82, Pittsburgh, PA, Aug. 1982, pp. 278-283.
[29] J. R. Gabriel, "Algorithms for automated diagnosis of faults in physical plant," Math. and Comput. Sci. Div. Rep., Argonne Nat. Lab., Argonne, IL, 1983.
[30] M. Gordon, "A very simple model of sequential behavior of nMOS," inVLSI 81, J. P. Gray, Ed. New York: Academic, 1981, pp. 85-94.
[31] J. P. Roth, "Automatic synthesis, verification and testing," inVLSI 81, J. P. Gray, Ed. New York: Academic, 1981, pp. 351-355.
[32] B. T. Smith, "Reference manual for the environmental theorem prover," Argonne, IL, to be published as an Argonne Tech. Rep.
[33] J. Kljaich, "Formal verification of digital systems," Ph.D. dissertation, Dep. Comput. Sci., Illinois, Instit. Technol., Dec. 1985.
[34] M. Gordon, R. Milner, and C. Wadsworth, "Edinburgh LCF: A mechanized logic of computation," inSpringer-Verlag, LNCS 79, MILN79.
[35] S. Dasgupta and A. Wagner, "The use of Hoare logic in the verification of microprograms,"Int. J. Comput. Inform. Sci., vol. 13, pp. 461-490, 1984.
[36] D. A. Patterson, "Strum: Structured microprogram development system for correct firmware,"IEEE Trans. Comput., vol. C-25, pp. 974-985, Oct. 1976.
[37] W. A. Woods, "What's important about knowledge representation?,"IEEE Computer, vol. 16, pp. 22-27, Oct. 1983.
[38] L. Wos, R. Overbeek, E. Lusk, and J. Boyle,Automated Reasoning: Introduction and Applications. Englewood Cliffs, NJ: Prentice-Hall, 1974.
[39] J. L. Peterson,Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.
[40] J. Meldman and A. Holt, "Petri nets and legal systems,"Jurimetrics J., vol. 12, pp. 65-75, Dec. 1972.
[41] R. A. Nelson, L. M. Haibt, and P. B. Sheridan, "Casting Petri nets into programs,"IEEE Trans. Software Eng., vol. SE-9, pp. 590- 602, Sept. 1983.
[42] P. Azema, R. Valette, and M. Diaz, "Petri nets as a common tool for design verification and hardware simulation," inProc. 13th Design Automat. Conf., San Francisco, CA, June 1976, pp. 109-116.
[43] Y. W. Han and W. L. Heimerdinger,Theory of Fault-Tolerance 1977 Final Report, Honeywell, Minneapolis, MN, 1977.
[44] W. L. Heimerdinger and Y. W. Han,A Graph Theoretic Approach to Fault-Tolerant Computing Final Report, Honeywell, Minneapolis, MN, 1977.
[45] H. J. Wojtkowiak, "Design automation and verification for digital systems," IBM Res. Rep., IBM T. J. Watson Research Center, Yorktown Heights, NY, 1980.
[46] H. J. Genrich and K. Lautenbach, "System modelling with high-level petri nets,"Theoret. Com. Sci., vol. 13, pp. 109-136, 1981.
[47] W. Kluge, "A unifying approach to computer system modelling based on Petri nets," in unpublished lecture notes.
[48] K. Zuse, "Petri-nets from the engineer's viewpoint Lectures I and II," inNet Theory and Applications. Berlin, Germany: Springer-Verlag, 1980, pp. 441-479.
[49] B. Mishra and E. M. Clarke, "Using temporal logic," Dep. Comput. Sci., Tech. Rep. CMU-CS-83-155, Carnegie-Mellon University, Pittsburgh, PA, Sept. 1983.
[50] P. Kawakami and R. McCarthy Eds.,Signetics Logic-TTL Data Manual, Signetics Corp., Sunnyvale, CA, 1978.
[51] C. L. Chang and R. C. T. Lee,Symbolic Logic and Mechanical Theorem Proving. New York: Academic, 1973.
[52] F. Hennie,Introduction to Computability. Reading, MA: Addision-Wesley, 1977.
[53] L. Wos, G. A. Robinson, and D. F. Carson, "Efficiency and completeness of the set of support strategy in theorem proving,"J. ACM, vol. 12, pp. 536-541, 1965.
[54] S. Winker, "Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions,"J. ACM, vol. 29, pp. 273-284, Apr. 1982.
[55] W. F. Clocksin and C. S. Mellish,Programming in Prolog. New York: Springer-Verlag, 1984.
[56] A. Avizienis, "Design diversity-The challenge of the eighties," inProc. 12th Annu. Int. Symp. Fault-Tolerant Comput., Santa Monica, CA, June 1982, pp. 44-45.

Index Terms:
fault tolerance; theorem-proving techniques; formal verification system; automated reasoning techniques; fault tolerant computing; theorem proving.
Citation:
J. Kljaich, Jr., B.T. Smith, A.S. Wojcik, "Formal Verification of Fault Tolerance Using Theorem-Proving Techniques," IEEE Transactions on Computers, vol. 38, no. 3, pp. 366-376, March 1989, doi:10.1109/12.21123
Usage of this product signifies your acceptance of the Terms of Use.