Formal validation of the GUARDS inter-consistency mechanism

In this paper we report the experience carried out to specify and validate the Inter-consistency mechanism developed within the European project GUARDS as a component of an architecture for embedded safety-critical systems. The validation approach is based on model checking technique and exploits the verification methodology supported by the JACK environment. The properties that guarantee the desired behaviour of the mechanism are specified as temporal logic formulae; the JACK model checker is then used to verify that the behaviour of the mechanism satisfies such properties also in presence of faults.