A model checker for performance and dependability properties


Hermanns, H. and Katoen, J.P. and Meyer-Kayser, J. and Siegle, M. (2001) A model checker for performance and dependability properties. In: 2nd PROGRESS workshop on Embedded Systems, 18 Oct 2001, Veldhoven, The Netherlands (pp. pp. 83-88).

open access
Abstract:Markov chains are widely used in the context of
performance and reliability evaluation of systems of various
nature. Model checking of such chains with respect to
a given (branching) temporal logic formula has been proposed
for both the discrete [8] and the continuous time setting
[1], [3]. In this short paper, we describe the prototype
model checker $E \vdash M C^2$ for discrete and continuous-time
Markov chains, where properties are expressed in appropriate
extensions of CTL.We illustrate the general benefits
of this approach and discuss the structure of the tool.
Item Type:Conference or Workshop Item
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66271
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page