Validating the Design of Dependable Systems

This paper reports an approach for the specification and verification of the correctness of dependable system designs achieved by the application of fault tolerant techniques based on equivalence relations and model checking techniques. The behaviour of the system in absence of faults is formally specified and faults are assumed as random events which interfere with the system by modifying its behaviour: The fault tolerant technique is formalized by a context, which specifies how replicas of the system cooperate to deal with faults. The system design is proved to satisfy the correctness property under a given fault hypothesis, by proving the observational equivalence between the system design specification and the fault-free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behaviour can be applied to verify the correctness of the design