Formal Performability Evaluation of Architectural Models of Critical Infrastructures
Haverkort, B.R. and Kuntz, M. and Remke, A. and Roolvink, S. (2010) Formal Performability Evaluation of Architectural Models of Critical Infrastructures. In: ESREL 2010 Annual Conference, 5-9 Sept 2010, Greece, Rhodos (pp. pp. 27-34).
Restricted to UT campus only : Request a copy
|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.
|Item Type:||Conference or Workshop Item|
|Copyright:||© 2010 Taylor & Francis|
Electrical Engineering, Mathematics and Computer Science (EEMCS)
|Link to this item:||http://purl.utwente.nl/publications/75313|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page