Implementing a Model Checker for Performability Behaviour


Hermanns, H. and Katoen, J.P. and Meyer-Kayser, J. (2001) Implementing a Model Checker for Performability Behaviour. In: Fifth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS 5), September 15-16, 2001, Erlangen, Germany (pp. pp. 110-114).

open access
Abstract:We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be verified are specified with the help of the action-based temporal logic aCSL. The technique is currently being implemented in our freely available prototype tool ETMCC.
Item Type:Conference or Workshop Item
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page