Title :
Formal verification of fault tolerance using theorem-proving techniques
Author :
Kljaich, Joseph, Jr. ; Smith, Brian T. ; Wojcik, Anthony S.
Author_Institution :
AT&T Bell Lab., Naperville, IL, USA
fDate :
3/1/1989 12:00:00 AM
Abstract :
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
Keywords :
fault tolerant computing; theorem proving; automated reasoning techniques; fault tolerance; formal verification system; theorem-proving techniques; Application software; Artificial intelligence; Digital systems; Fault tolerance; Fault tolerant systems; Formal verification; Hardware; Laboratories; Petri nets; Timing;
Journal_Title :
Computers, IEEE Transactions on