Formal Dependability Engineering with MIOA

Matthias Kuntz; Boudewijn Haverkort

Formal Dependability Engineering with MIOA

Research output: Book/Report › Report › Professional

37 Downloads (Pure)

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 language	English
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	25
Publication status	Published - 4 Jun 2008

Publication series

Name	CTIT Technical Report Series
Publisher	Centre for Telematics and Information Technology, University of Twente
No.	274/TR-CTIT-08-39
ISSN (Print)	1381-3625

Access to Document

ReportFinal published version, 280 KB

Cite this

@book{472e615e9a914551881ad8b8914bf7cc,

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

author = "Matthias Kuntz and Boudewijn Haverkort",

year = "2008",

month = jun,

day = "4",

language = "English",

series = "CTIT Technical Report Series",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "274/TR-CTIT-08-39",

address = "Netherlands",

}

TY - BOOK

T1 - Formal Dependability Engineering with MIOA

AU - Kuntz, Matthias

AU - Haverkort, Boudewijn

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.

M3 - Report

T3 - CTIT Technical Report Series

BT - Formal Dependability Engineering with MIOA

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Formal Dependability Engineering with MIOA

Abstract

Publication series

Access to Document

Fingerprint

Cite this