The authors first provide some background on the formal verification of fault tolerance. Then they describe an extended Petri net method of representation that encompasses token value, typed transitions and places (defining behavioral properties), specialized places, the association of control signals with transitions, and real-world constraints on flow extensions. They propose a method of validating fault tolerance that exploits this representation formalism, and they use a theorem prover to automate their verification strategy. The theorem prover takes the explicit hypotheses and axioms, defines a fault-tolerant machine, and uses this hypothetical computer to test for inconsistencies.

The authors give a concise example that compares the proposed methodology with the Draper Laboratory Fault Tolerant Processor. They hope to refine their work to include avoiding subgoal interaction of assumptions, verifying properties other than fault tolerance, and applying their methodology to software. But even at the present stage of research, their verification technique demonstrates its applicability to nontrivial computing systems. Although they do not explicitly address the possibility, one can interpolate how such a methodology could be incorporated into a design tool.