Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking

Share/Save/Bookmark

Gnesi, S. and Lenzini, G. and Martinelli, F. (2003) Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking. In: Electronic Notes in Theoretical Computer Science (ENTCS), Int. Workshop on Software Verification and Validation (SVV), Mumbai, India.

[img]
Preview
PDF
300Kb
Abstract:This paper presents a framework for a logical characterisation of fault tolerance and its formal analysis based on partial model checking techniques. The framework requires a fault tolerant system to be modelled using a formal calculus, here the CCS process algebra. To this aim we propose a uniform modelling 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 characterisation 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 on any particular fault assumption. Moreover this logical characterisation 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.
Item Type:Conference or Workshop Item
Link to this item:http://purl.utwente.nl/publications/55555
Official URL:http://dx.doi.org/10.1016/j.entcs.2004.09.032
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page