Istituto di Informatica e Telematica     
Gnesi S., Lenzini G., Martinelli F. Logical Specification and Analysis of Fault Tolerant Systems Through Partial Model Checking. In: ENTCS, vol. 118 pp. 57 - 70. Elsevier Science Publishers Ltd. Essex, UK, 2005.
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.
DOI: 10.1016/j.entcs.2004.09.032
Subject Fault Tolerant Systems
Formal Verification
Partial Model Checking
K.6.5 Security and Protection

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional