Formal Dependability Engineering with MIOA

Research output: Book/ReportBookScientific

Abstract

In this paper, we introduce MIOA, a stochastic process algebra-like specification language with datatypes, as well as a logic intSPDL, and its model checking algorithms. MIOA, which stands for Markovian input/output automata language, is an extension of Lynch's input/automata with Markovian timed transitions.MIOA can serve both as a fully fledged ``stand-alone'' specification language and the semantic model for the architectural dependability modelling and evaluation language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, to deal with the specialties of MIOA. intSPDL in the context of Arcade 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 show examples of applying MIOA and intSPDL in the realm of dependability modelling with Arcade.
Original languageEnglish
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Publication statusPublished - 4 Jun 2008
Externally publishedYes

Publication series

NameCTIT Technical Report Series

Fingerprint

Specification languages
Semantics
Model checking
Random processes
Algebra

Keywords

  • METIS-250986
  • EWI-12786
  • IR-64777

Cite this

Kuntz, G. W. M., & Haverkort, B. R. H. M. (2008). Formal Dependability Engineering with MIOA. (CTIT Technical Report Series). Enschede: Centre for Telematics and Information Technology (CTIT).
Kuntz, G.W.M. ; Haverkort, Boudewijn R.H.M. / Formal Dependability Engineering with MIOA. Enschede : Centre for Telematics and Information Technology (CTIT), 2008. (CTIT Technical Report Series).
@book{401f08735e5747d1bf490313a36644c1,
title = "Formal Dependability Engineering with MIOA",
abstract = "In this paper, we introduce MIOA, a stochastic process algebra-like specification language with datatypes, as well as a logic intSPDL, and its model checking algorithms. MIOA, which stands for Markovian input/output automata language, is an extension of Lynch's input/automata with Markovian timed transitions.MIOA can serve both as a fully fledged ``stand-alone'' specification language and the semantic model for the architectural dependability modelling and evaluation language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, to deal with the specialties of MIOA. intSPDL in the context of Arcade 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 show examples of applying MIOA and intSPDL in the realm of dependability modelling with Arcade.",
keywords = "METIS-250986, EWI-12786, IR-64777",
author = "G.W.M. Kuntz and Haverkort, {Boudewijn R.H.M.}",
year = "2008",
month = "6",
day = "4",
language = "English",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",

}

Kuntz, GWM & Haverkort, BRHM 2008, Formal Dependability Engineering with MIOA. CTIT Technical Report Series, Centre for Telematics and Information Technology (CTIT), Enschede.

Formal Dependability Engineering with MIOA. / Kuntz, G.W.M.; Haverkort, Boudewijn R.H.M.

Enschede : Centre for Telematics and Information Technology (CTIT), 2008. (CTIT Technical Report Series).

Research output: Book/ReportBookScientific

TY - BOOK

T1 - Formal Dependability Engineering with MIOA

AU - Kuntz, G.W.M.

AU - Haverkort, Boudewijn R.H.M.

PY - 2008/6/4

Y1 - 2008/6/4

N2 - In this paper, we introduce MIOA, a stochastic process algebra-like specification language with datatypes, as well as a logic intSPDL, and its model checking algorithms. MIOA, which stands for Markovian input/output automata language, is an extension of Lynch's input/automata with Markovian timed transitions.MIOA can serve both as a fully fledged ``stand-alone'' specification language and the semantic model for the architectural dependability modelling and evaluation language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, to deal with the specialties of MIOA. intSPDL in the context of Arcade 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 show examples of applying 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 datatypes, as well as a logic intSPDL, and its model checking algorithms. MIOA, which stands for Markovian input/output automata language, is an extension of Lynch's input/automata with Markovian timed transitions.MIOA can serve both as a fully fledged ``stand-alone'' specification language and the semantic model for the architectural dependability modelling and evaluation language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, to deal with the specialties of MIOA. intSPDL in the context of Arcade 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 show examples of applying MIOA and intSPDL in the realm of dependability modelling with Arcade.

KW - METIS-250986

KW - EWI-12786

KW - IR-64777

M3 - Book

T3 - CTIT Technical Report Series

BT - Formal Dependability Engineering with MIOA

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Kuntz GWM, Haverkort BRHM. Formal Dependability Engineering with MIOA. Enschede: Centre for Telematics and Information Technology (CTIT), 2008. (CTIT Technical Report Series).