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

S. Gnesi, G. Lenzini, F. Martinelli

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    41 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationProceedings of the International Workshop on Software Verification and Validation (SVV 2003)
    EditorsS. Etalle, S. Mukhopadhyay, A. Roychoudhury
    Place of PublicationAmsterdam
    PublisherElsevier
    Pages57-70
    Number of pages14
    DOIs
    Publication statusPublished - 2003
    EventInternational Workshop on Software Verification and Validation, SVV 2003 - Mumbai, India
    Duration: 14 Dec 200314 Dec 2003

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    PublisherElsevier
    Volume118
    ISSN (Print)1571-0661

    Conference

    ConferenceInternational Workshop on Software Verification and Validation, SVV 2003
    Abbreviated titleSVV
    CountryIndia
    CityMumbai
    Period14/12/0314/12/03

    Keywords

    • Fault tolerant systems
    • Formal verification
    • Partial model checking

    Fingerprint Dive into the research topics of 'Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking'. Together they form a unique fingerprint.

  • Cite this

    Gnesi, S., Lenzini, G., & Martinelli, F. (2003). Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking. In S. Etalle, S. Mukhopadhyay, & A. Roychoudhury (Eds.), Proceedings of the International Workshop on Software Verification and Validation (SVV 2003) (pp. 57-70). (Electronic Notes in Theoretical Computer Science; Vol. 118). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2004.09.032