Argonne National Lab., IL., Report No. CONF-870399-1, 1987.
Abstract: In an earlier paper the author has described the hierarchical modeling technique based upon Petri nets, and the formal analysis techniques based upon the automated reasoning software ITP/LMA. In this paper, the author demonstrates that the same modeling and analysis techniques apply to proving the fault-tolerance of the software. The approach that has been developed has provided insight into formal software specification as well as into the generation of test vectors for software.