A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains

H. Boudali, P Crouzen, Mariëlle Ida Antoinette Stoelinga

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

    61 Citations (Scopus)
    102 Downloads (Pure)

    Abstract

    Dynamic fault trees (DFTs) are a versatile and common formalism to model and analyze the reliability of computer-based systems. This paper presents a formal semantics of DFTs in terms of input/output interactive Markov chains (I/O-IMCs), which extend continuous-time Markov chains with discrete input, output and internal actions. This semantics provides a rigorous basis for the analysis of DFTs. Our semantics is fully compositional, that is, the semantics of a DFT is expressed in terms of the semantics of its elements (i.e. basic events and gates). This enables an efficient analysis of DFTs through compositional aggregation, which helps to alleviate the state-space explosion problem by incrementally building the DFT state space. We have implemented our methodology by developing a tool, and showed, through four case studies, the feasibility of our approach and its effectiveness in reducing the state space to be analyzed.
    Original languageEnglish
    Title of host publicationAutomated Technology for Verification and Analysis
    Subtitle of host publication5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings
    EditorsKedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura
    Place of PublicationBerlin
    PublisherSpringer
    Pages441-456
    Number of pages16
    ISBN (Electronic)978-3-540-75596-8
    ISBN (Print)978-3-540-75595-1
    DOIs
    Publication statusPublished - Oct 2007
    Event5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007 - Tokyo, Japan
    Duration: 22 Oct 200725 Oct 2007
    Conference number: 5

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume4762
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007
    Abbreviated titleATVA
    CountryJapan
    CityTokyo
    Period22/10/0725/10/07

    Keywords

    • EWI-11031
    • METIS-241898
    • IR-64340

    Fingerprint Dive into the research topics of 'A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains'. Together they form a unique fingerprint.

    Cite this