
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
J. Kljaich, Jr., B.T. Smith, A.S. Wojcik, "Formal Verification of Fault Tolerance Using TheoremProving Techniques," IEEE Transactions on Computers, vol. 38, no. 3, pp. 366376, March, 1989.  
BibTex  x  
@article{ 10.1109/12.21123, author = {J. Kljaich, Jr. and B.T. Smith and A.S. Wojcik}, title = {Formal Verification of Fault Tolerance Using TheoremProving Techniques}, journal ={IEEE Transactions on Computers}, volume = {38}, number = {3}, issn = {00189340}, year = {1989}, pages = {366376}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.21123}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Formal Verification of Fault Tolerance Using TheoremProving Techniques IS  3 SN  00189340 SP366 EP376 EPD  366376 A1  J. Kljaich, Jr., A1  B.T. Smith, A1  A.S. Wojcik, PY  1989 KW  fault tolerance; theoremproving techniques; formal verification system; automated reasoning techniques; fault tolerant computing; theorem proving. VL  38 JA  IEEE Transactions on Computers ER   
[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. SE10, pp. 825836, Nov. 1984.
[2] C. J. Kooman, "Algebraic specification and verification of communication protocols,"Sci. Comput. Programming, vol. 5, pp. 136, Feb. 1985.
[3] Barrow, H.G., "Verify: A Program for Proving Correctness of Digital Hardware Designs,"Artificial Intelligence, Vol. 24, 1984, pp. 437491.
[4] J.A. Darringer, "The Application of Program Verification Techniques to Hardware Verification,"Proc. ACM IEEE 16th Design Automation Conf., June 1979, pp. 375381.
[5] M. Gordon, "A model of register transfer systems with applications to microcode and VLSI correctness," Dep. Comput. Sci. Int. Rep. CSR 8281, Univ. of Edinburgh, Edinburgh, England, 1981.
[6] L. Haynes, "Logic design verification using static analysis," Ph.D. dissertation, Dep. Elec. Eng., Univ. Illinois, UrbanaChampaign, IL, May 1983.
[7] M. Monachino, "Design verification system for large scale LSI designs,"IBM J. Res. Develop., vol. 26, pp. 8999, Jan 1982.
[8] V. Pitchumani and E. P. Stabler, "An inductive assertion method for register transfer level design verification,"IEEE Trans. Comput., vol. C32, pp. 10731080, Dec. 1983.
[9] T. J. Wagner, "Hardware verification," Ph.D. dissertation, STANCS77632, Stanford Univ., 1977.
[10] A. Wojcik, "Formal Design Verification of Digital Systems,"Proc. Design Automation Conf., 1983, pp. 246252.
[11] Wojcik, A.S., "A Formal Design Verification System Based on an Automated Reasoning System,"ACM IEEE 21st Design Automation Conf., July 1984, pp. 641647.
[12] K. R. Apt, "Ten years of Hoare'slogic: A surveyPart one,"ACM Trans. Program. Lang. Syst., vol. 3, pp. 431483, 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. 97147, June 1972.
[14] J. C. King, "Symbolic execution and program testing,"Commun. ACM, vol. 19, no. 7, pp. 385394, 1976.
[15] M. H. Cheheyl, M. Gasser, G. A. Huff, and J. K. Millen, "Verifying security,"ACM Comput. Surveys, vol. 13, pp. 279339, Sept. 1981.
[16] C.E. Landwehr, "Formal Models of Computer Security,"ACM Computer Surveys SIGOPS, Sept. 1981, pp. 247278.
[17] T. B. Smith, "Fault tolerant processor concepts and operation," inProc. 14th Annu. Int. Conf. FaultTolerant Comput., Kissimmee, FL, June 1984, pp. 158163.
[18] E. L. Lusk and R. A. Overbeek, "An LMAbased 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. 139147.
[22] A. E. Ruehli and G. S. Ditlow, "Circuit analysis, logic simulation, and design verification for VLSI,"Proc. IEEE, vol. 71, pp. 3448, 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. 315320.
[24] M. H. Doshi, R. B. Sullivan, and D. M. Schuler, "THEMIS logic simulatorA mix mode, multilevel, hiearchica., interactive digital circuit simulator," inProc. 21st Design Automat. Conf., Albuquerque, NM, June 1984, pp. 2431.
[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. 431434.
[26] G. H. Chisholm, J. Kljaich, B. T. Smith, and A. S. Wojcik, "An approach to the verification of a faulttolerant, computerbased, reactor safety systemA 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. 432440, Sept.Oct. 1985.
[28] M. G. Genesereth, "Diagnosis using hierarchical design models," inProc. 1982 Nat. Conf. Artif. Intell. AAAI82, Pittsburgh, PA, Aug. 1982, pp. 278283.
[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. 8594.
[31] J. P. Roth, "Automatic synthesis, verification and testing," inVLSI 81, J. P. Gray, Ed. New York: Academic, 1981, pp. 351355.
[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," inSpringerVerlag, 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. 461490, 1984.
[36] D. A. Patterson, "Strum: Structured microprogram development system for correct firmware,"IEEE Trans. Comput., vol. C25, pp. 974985, Oct. 1976.
[37] W. A. Woods, "What's important about knowledge representation?,"IEEE Computer, vol. 16, pp. 2227, Oct. 1983.
[38] L. Wos, R. Overbeek, E. Lusk, and J. Boyle,Automated Reasoning: Introduction and Applications. Englewood Cliffs, NJ: PrenticeHall, 1974.
[39] J. L. Peterson,Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: PrenticeHall, 1981.
[40] J. Meldman and A. Holt, "Petri nets and legal systems,"Jurimetrics J., vol. 12, pp. 6575, Dec. 1972.
[41] R. A. Nelson, L. M. Haibt, and P. B. Sheridan, "Casting Petri nets into programs,"IEEE Trans. Software Eng., vol. SE9, 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. 109116.
[43] Y. W. Han and W. L. Heimerdinger,Theory of FaultTolerance 1977 Final Report, Honeywell, Minneapolis, MN, 1977.
[44] W. L. Heimerdinger and Y. W. Han,A Graph Theoretic Approach to FaultTolerant 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 highlevel petri nets,"Theoret. Com. Sci., vol. 13, pp. 109136, 1981.
[47] W. Kluge, "A unifying approach to computer system modelling based on Petri nets," in unpublished lecture notes.
[48] K. Zuse, "Petrinets from the engineer's viewpoint Lectures I and II," inNet Theory and Applications. Berlin, Germany: SpringerVerlag, 1980, pp. 441479.
[49] B. Mishra and E. M. Clarke, "Using temporal logic," Dep. Comput. Sci., Tech. Rep. CMUCS83155, CarnegieMellon University, Pittsburgh, PA, Sept. 1983.
[50] P. Kawakami and R. McCarthy Eds.,Signetics LogicTTL 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: AddisionWesley, 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. 536541, 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. 273284, Apr. 1982.
[55] W. F. Clocksin and C. S. Mellish,Programming in Prolog. New York: SpringerVerlag, 1984.
[56] A. Avizienis, "Design diversityThe challenge of the eighties," inProc. 12th Annu. Int. Symp. FaultTolerant Comput., Santa Monica, CA, June 1982, pp. 4445.