Automated Verification of Fault Tolerant Mechanisms

In this paper we report the experience carried out to specify and validate the Inter-consistency fault tolerance mechanism proposed in the GUARDS project [14]. The validation approach is based on model checking technique and exploits the verification methodology supported by the JACK environment [5]. In this approach, the behaviour of the Inter-consistency mechanism is specified as a network of processes, defined in a process algebra or, graphically, as Labelled Transition Systems. Using the JACK tools the global finite state model of the behaviour of the mechanism is produced. In this model, actions modeling the occurrences of faults are included, following some fault assumptions that can be modified to study the behaviour of the mechanism under different fault hypotheses. The properties that guarantee the desired behaviour of the mechanism are then specified as temporal logic formulae; the JACK model checker allows us to verify that the behaviour of the mechanism satisfies such properties also in presence of faults conformant to the fault assumptions.