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

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

doi:10.1007/978-3-540-75596-8_31

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 proceeding › Conference contribution › Academic › peer-review

74 Citations (Scopus)

117 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 language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings
Editors	Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura
Place of Publication	Berlin
Publisher	Springer
Pages	441-456
Number of pages	16
ISBN (Electronic)	978-3-540-75596-8
ISBN (Print)	978-3-540-75595-1
DOIs	https://doi.org/10.1007/978-3-540-75596-8_31
Publication status	Published - Oct 2007
Event	5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007 - Tokyo, Japan Duration: 22 Oct 2007 → 25 Oct 2007 Conference number: 5

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4762
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007
Abbreviated title	ATVA
Country/Territory	Japan
City	Tokyo
Period	22/10/07 → 25/10/07

Keywords

EWI-11031
METIS-241898
IR-64340

Access to Document

10.1007/978-3-540-75596-8_31

ATVA07-BoudaliAccepted author version, 322 KB

Cite this

Boudali, H., Crouzen, P., & Stoelinga, M. I. A. (2007). A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains. In K. S. Namjoshi, T. Yoneda, T. Higashino, & Y. Okamura (Eds.), Automated Technology for Verification and Analysis: 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings (pp. 441-456). (Lecture Notes in Computer Science; Vol. 4762). Springer. https://doi.org/10.1007/978-3-540-75596-8_31

Boudali, H. ; Crouzen, P ; Stoelinga, Mariëlle Ida Antoinette. / A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains. Automated Technology for Verification and Analysis: 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings. editor / Kedar S. Namjoshi ; Tomohiro Yoneda ; Teruo Higashino ; Yoshio Okamura. Berlin : Springer, 2007. pp. 441-456 (Lecture Notes in Computer Science).

@inproceedings{573ae7b712774ba9a99884ced87ee47e,

title = "A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains",

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.",

keywords = "EWI-11031, METIS-241898, IR-64340",

author = "H. Boudali and P Crouzen and Stoelinga, {Mari{\"e}lle Ida Antoinette}",

year = "2007",

month = oct,

doi = "10.1007/978-3-540-75596-8_31",

language = "English",

isbn = "978-3-540-75595-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "441--456",

editor = "Namjoshi, {Kedar S.} and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura",

booktitle = "Automated Technology for Verification and Analysis",

note = "5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007, ATVA ; Conference date: 22-10-2007 Through 25-10-2007",

}

Boudali, H, Crouzen, P & Stoelinga, MIA 2007, A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains. in KS Namjoshi, T Yoneda, T Higashino & Y Okamura (eds), Automated Technology for Verification and Analysis: 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings. Lecture Notes in Computer Science, vol. 4762, Springer, Berlin, pp. 441-456, 5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007, Tokyo, Japan, 22/10/07. https://doi.org/10.1007/978-3-540-75596-8_31

A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains. / Boudali, H.; Crouzen, P; Stoelinga, Mariëlle Ida Antoinette.
Automated Technology for Verification and Analysis: 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings. ed. / Kedar S. Namjoshi; Tomohiro Yoneda; Teruo Higashino; Yoshio Okamura. Berlin: Springer, 2007. p. 441-456 (Lecture Notes in Computer Science; Vol. 4762).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Boudali, H.

AU - Crouzen, P

AU - Stoelinga, Mariëlle Ida Antoinette

N1 - Conference code: 5

PY - 2007/10

Y1 - 2007/10

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

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

KW - EWI-11031

KW - METIS-241898

KW - IR-64340

U2 - 10.1007/978-3-540-75596-8_31

DO - 10.1007/978-3-540-75596-8_31

M3 - Conference contribution

SN - 978-3-540-75595-1

T3 - Lecture Notes in Computer Science

SP - 441

EP - 456

BT - Automated Technology for Verification and Analysis

A2 - Namjoshi, Kedar S.

A2 - Yoneda, Tomohiro

A2 - Higashino, Teruo

A2 - Okamura, Yoshio

PB - Springer

CY - Berlin

T2 - 5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007

Y2 - 22 October 2007 through 25 October 2007

ER -

Boudali H, Crouzen P, Stoelinga MIA. A compositional semantics for Dynamic Fault Trees in terms of Interactive Markov Chains. In Namjoshi KS, Yoneda T, Higashino T, Okamura Y, editors, Automated Technology for Verification and Analysis: 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings. Berlin: Springer. 2007. p. 441-456. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-75596-8_31

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this