Logical specification and analysis of fault tolerant systems through partial model checking

This paper presents a framework for a logical characterization of fault tolerance and its formal analysis based on partial model checking techniques. The framework requires a fault tolerant system to be modeled using a formal calculus, here the CCS process algebra. To this aim we propose a uniform modeling scheme in which to specify a formal model of the system, its failing behaviour and possibly its fault-recovering procedures. Once a formal model is provided into our scheme, fault tolerance - with respect to a given property - can be formalized as an equational µ-calculus formula. This formula expresses, in a logic formalism, all the fault scenarios satisfying that fault tolerance property. Such a characterization understands the analysis of fault tolerance as a form of analysis of open systems and, thank to partial model checking strategies, it can be made independent from any particular fault assumption. Moreover this logical characterization makes possible the fault-tolerance verification problem be expressed as a general µ-calculus validation problem, for solving which many theorem proof techniques and tools are available. We present several analysis methods showing the flexibility of our approach.