Formal reasoning on fault coverage of fault tolerant techniques: A case study

Abstract

In this paper we show how a formal reasoning can be applied for studying the fault coverage of a fault tolerant technique when the behaviour of a system with a set of predefined faults is considered. This method is based on process algebras and equivalence theory. 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. A fault tolerant technique can be proved to tolerate the set of predefined faults iff the actual behaviour of the system is the same as the behaviour of the system in absence of faults. The approach is illustrated by considering the design of a stable storage disk.