Structural analysis of explicit fault-tolerant programs

Explicit fault tolerant programs are characterized by proactive efforts to ensure robustness and ability of fault correction. A fault tolerant application is usually realized conforming to one of a collection of standard techniques. Graph based methods can be used to examine existing applications to derive a control flow abstraction with respect to the fault-tolerance architecture. This abstraction, which we call the fault tolerance behavioural type, can be used as basis of structural analysis of the implemented architecture. This paper outlines the basic ideas and demonstrates their application using CTL (Computation Tree Logic) model checking to verify fault tolerance properties of explicit fault-tolerant programs.