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

S. Gnesi, Sandro Etalle (Editor), S. Mukhopadhyay (Editor), Gabriele Lenzini, G. Lenzini, F. Martinelli, A. Roychoudhury (Editor)

    Research output: Contribution to conferencePaper

    36 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 languageUndefined
    Pages57-70
    Number of pages14
    DOIs
    Publication statusPublished - Dec 2003
    EventInternational Workshop on Software Verification and Validation: SVV 2003 - Mumbai, India
    Duration: 14 Dec 200314 Dec 2003

    Conference

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

    Keywords

    • IR-55555
    • EWI-828

    Cite this

    Gnesi, S., Etalle, S. (Ed.), Mukhopadhyay, S. (Ed.), Lenzini, G., Lenzini, G., Martinelli, F., & Roychoudhury, A. (Ed.) (2003). Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking. 57-70. Paper presented at International Workshop on Software Verification and Validation, Mumbai, India. https://doi.org/10.1016/j.entcs.2004.09.032
    Gnesi, S. ; Etalle, Sandro (Editor) ; Mukhopadhyay, S. (Editor) ; Lenzini, Gabriele ; Lenzini, G. ; Martinelli, F. ; Roychoudhury, A. (Editor). / Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking. Paper presented at International Workshop on Software Verification and Validation, Mumbai, India.14 p.
    @conference{89baad5fe138491d9b7822a9680e39ec,
    title = "Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking",
    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.",
    keywords = "IR-55555, EWI-828",
    author = "S. Gnesi and Sandro Etalle and S. Mukhopadhyay and Gabriele Lenzini and G. Lenzini and F. Martinelli and A. Roychoudhury",
    note = "Imported from DIES; null ; Conference date: 14-12-2003 Through 14-12-2003",
    year = "2003",
    month = "12",
    doi = "10.1016/j.entcs.2004.09.032",
    language = "Undefined",
    pages = "57--70",

    }

    Gnesi, S, Etalle, S (ed.), Mukhopadhyay, S (ed.), Lenzini, G, Lenzini, G, Martinelli, F & Roychoudhury, A (ed.) 2003, 'Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking' Paper presented at International Workshop on Software Verification and Validation, Mumbai, India, 14/12/03 - 14/12/03, pp. 57-70. https://doi.org/10.1016/j.entcs.2004.09.032

    Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking. / Gnesi, S.; Etalle, Sandro (Editor); Mukhopadhyay, S. (Editor); Lenzini, Gabriele; Lenzini, G.; Martinelli, F.; Roychoudhury, A. (Editor).

    2003. 57-70 Paper presented at International Workshop on Software Verification and Validation, Mumbai, India.

    Research output: Contribution to conferencePaper

    TY - CONF

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

    AU - Gnesi, S.

    AU - Lenzini, Gabriele

    AU - Lenzini, G.

    AU - Martinelli, F.

    A2 - Etalle, Sandro

    A2 - Mukhopadhyay, S.

    A2 - Roychoudhury, A.

    N1 - Imported from DIES

    PY - 2003/12

    Y1 - 2003/12

    N2 - 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.

    AB - 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.

    KW - IR-55555

    KW - EWI-828

    U2 - 10.1016/j.entcs.2004.09.032

    DO - 10.1016/j.entcs.2004.09.032

    M3 - Paper

    SP - 57

    EP - 70

    ER -

    Gnesi S, Etalle S, (ed.), Mukhopadhyay S, (ed.), Lenzini G, Lenzini G, Martinelli F et al. Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking. 2003. Paper presented at International Workshop on Software Verification and Validation, Mumbai, India. https://doi.org/10.1016/j.entcs.2004.09.032