Formal verification of fault tolerance using theorem-proving techniques
J. Kljaich, Brian T. Smith, Anthony S. Wojcik · IEEE Transactions on Computers · 1989
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 capabilities of the formal verification system under development.>