Formal verification of fault tolerance using theorem-proving techniques

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.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>