Formal Performability Evaluation of Architectural Models of Critical Infrastructures

Boudewijn R.H.M. Haverkort; G.W.M. Kuntz; Anne Katharina Ingrid Remke; S. Roolvink; Ben J.M. Ale; Ioannis A. Papazoglou; Enrico Zio

Formal Performability Evaluation of Architectural Models of Critical Infrastructures

Boudewijn R.H.M. Haverkort, G.W.M. Kuntz, Anne Katharina Ingrid Remke, S. Roolvink, Ben J.M. Ale (Editor), Ioannis A. Papazoglou (Editor), Enrico Zio (Editor)

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

Abstract

In this paper, we introduce MIOA, a stochastic process algebra-like specification language with finite-domain datatypes, as well as the logic intSPDL, and its model checking algorithms. MIOA which stands for Markovian input/output automata language is an extension of Lynch’s input/output automata with Markovian timed transitions. MIOA can serve both as a fully fledged “stand-alone‿ specification language and as the semantic model for the architectural dependability description language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, designed to deal with the specialties of MIOA. In the context of Arcade, intSPDL can be seen as the semantic model of abstract and complex dependability measures that can be defined in the Arcade framework. We define syntax and semantics of both MIOA and intSPDL, and present application examples of MIOA and intSPDL in the realm of dependability modelling with Arcade.

Original language	English
Title of host publication	Proceedings of the ESREL 2010 Annual Conference
Place of Publication	London
Publisher	Taylor & Francis
Pages	27-34
Number of pages	8
ISBN (Print)	978-0-415-60427-7
Publication status	Published - 5 Sept 2010
Externally published	Yes

Keywords

IR-75313
CR-B.1.3
EWI-18358
METIS-276085

Cite this

@inproceedings{8b6c87b19f50424287590c825d8dd813,

title = "Formal Performability Evaluation of Architectural Models of Critical Infrastructures",

abstract = "In this paper, we introduce MIOA, a stochastic process algebra-like specification language with finite-domain datatypes, as well as the logic intSPDL, and its model checking algorithms. MIOA which stands for Markovian input/output automata language is an extension of Lynch{\textquoteright}s input/output automata with Markovian timed transitions. MIOA can serve both as a fully fledged “stand-alone‿ specification language and as the semantic model for the architectural dependability description language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, designed to deal with the specialties of MIOA. In the context of Arcade, intSPDL can be seen as the semantic model of abstract and complex dependability measures that can be defined in the Arcade framework. We define syntax and semantics of both MIOA and intSPDL, and present application examples of MIOA and intSPDL in the realm of dependability modelling with Arcade.",

keywords = "IR-75313, CR-B.1.3, EWI-18358, METIS-276085",

author = "Haverkort, {Boudewijn R.H.M.} and G.W.M. Kuntz and Remke, {Anne Katharina Ingrid} and S. Roolvink and Ale, {Ben J.M.} and Papazoglou, {Ioannis A.} and Enrico Zio",

year = "2010",

month = sep,

day = "5",

language = "English",

isbn = "978-0-415-60427-7",

pages = "27--34",

booktitle = "Proceedings of the ESREL 2010 Annual Conference",

publisher = "Taylor & Francis",

}

Formal Performability Evaluation of Architectural Models of Critical Infrastructures. / Haverkort, Boudewijn R.H.M.; Kuntz, G.W.M.; Remke, Anne Katharina Ingrid et al.
Proceedings of the ESREL 2010 Annual Conference. London: Taylor & Francis, 2010. p. 27-34.

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

TY - GEN

T1 - Formal Performability Evaluation of Architectural Models of Critical Infrastructures

AU - Haverkort, Boudewijn R.H.M.

AU - Kuntz, G.W.M.

AU - Remke, Anne Katharina Ingrid

AU - Roolvink, S.

A2 - Ale, Ben J.M.

A2 - Papazoglou, Ioannis A.

A2 - Zio, Enrico

PY - 2010/9/5

Y1 - 2010/9/5

N2 - In this paper, we introduce MIOA, a stochastic process algebra-like specification language with finite-domain datatypes, as well as the logic intSPDL, and its model checking algorithms. MIOA which stands for Markovian input/output automata language is an extension of Lynch’s input/output automata with Markovian timed transitions. MIOA can serve both as a fully fledged “stand-alone‿ specification language and as the semantic model for the architectural dependability description language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, designed to deal with the specialties of MIOA. In the context of Arcade, intSPDL can be seen as the semantic model of abstract and complex dependability measures that can be defined in the Arcade framework. We define syntax and semantics of both MIOA and intSPDL, and present application examples of MIOA and intSPDL in the realm of dependability modelling with Arcade.

AB - In this paper, we introduce MIOA, a stochastic process algebra-like specification language with finite-domain datatypes, as well as the logic intSPDL, and its model checking algorithms. MIOA which stands for Markovian input/output automata language is an extension of Lynch’s input/output automata with Markovian timed transitions. MIOA can serve both as a fully fledged “stand-alone‿ specification language and as the semantic model for the architectural dependability description language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, designed to deal with the specialties of MIOA. In the context of Arcade, intSPDL can be seen as the semantic model of abstract and complex dependability measures that can be defined in the Arcade framework. We define syntax and semantics of both MIOA and intSPDL, and present application examples of MIOA and intSPDL in the realm of dependability modelling with Arcade.

KW - IR-75313

KW - CR-B.1.3

KW - EWI-18358

KW - METIS-276085

M3 - Conference contribution

SN - 978-0-415-60427-7

SP - 27

EP - 34

BT - Proceedings of the ESREL 2010 Annual Conference

PB - Taylor & Francis

CY - London

ER -

Formal Performability Evaluation of Architectural Models of Critical Infrastructures

Abstract

Keywords

Fingerprint

Cite this