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: Other contributionOther research output

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 languageEnglish
PublisherTaylor & Francis
Number of pages8
Place of PublicationLondon
ISBN (Print)978-0-415-60427-7
Publication statusPublished - 5 Sep 2010
Externally publishedYes

Fingerprint

Critical infrastructures
Specification languages
Semantics
Model checking
Random processes
Algebra

Keywords

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

Cite this

Haverkort, B. R. H. M., Kuntz, G. W. M., Remke, A. K. I., Roolvink, S., Ale, B. J. M. (Ed.), Papazoglou, I. A. (Ed.), & Zio, E. (Ed.) (2010, Sep 5). Formal Performability Evaluation of Architectural Models of Critical Infrastructures. London: Taylor & Francis.
Haverkort, Boudewijn R.H.M. ; Kuntz, G.W.M. ; Remke, Anne Katharina Ingrid ; Roolvink, S. ; Ale, Ben J.M. (Editor) ; Papazoglou, Ioannis A. (Editor) ; Zio, Enrico (Editor). / Formal Performability Evaluation of Architectural Models of Critical Infrastructures. 2010. London : Taylor & Francis. 8 p.
@misc{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’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 = "9",
day = "5",
language = "English",
isbn = "978-0-415-60427-7",
publisher = "Taylor & Francis",
type = "Other",

}

Haverkort, BRHM, Kuntz, GWM, Remke, AKI, Roolvink, S, Ale, BJM (ed.), Papazoglou, IA (ed.) & Zio, E (ed.) 2010, Formal Performability Evaluation of Architectural Models of Critical Infrastructures. Taylor & Francis, London.

Formal Performability Evaluation of Architectural Models of Critical Infrastructures. / Haverkort, Boudewijn R.H.M.; Kuntz, G.W.M.; Remke, Anne Katharina Ingrid; Roolvink, S.; Ale, Ben J.M. (Editor); Papazoglou, Ioannis A. (Editor); Zio, Enrico (Editor).

8 p. London : Taylor & Francis. 2010, .

Research output: Other contributionOther research output

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 - Other contribution

SN - 978-0-415-60427-7

PB - Taylor & Francis

CY - London

ER -

Haverkort BRHM, Kuntz GWM, Remke AKI, Roolvink S, Ale BJM, (ed.), Papazoglou IA, (ed.) et al. Formal Performability Evaluation of Architectural Models of Critical Infrastructures. 2010. 8 p.