Issue No. 03 - March (1989 vol. 38)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.21123
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
fault tolerance; theorem-proving techniques; formal verification system; automated reasoning techniques; fault tolerant computing; theorem proving.
A. Wojcik, B. Smith and J. Kljaich, Jr., "Formal Verification of Fault Tolerance Using Theorem-Proving Techniques," in IEEE Transactions on Computers, vol. 38, no. , pp. 366-376, 1989.