On the Use of Model Checking Techniques for Quantitative Dependability Evaluation


Haverkort, Boudewijn R. and Hermanns, Holger and Katoen, Joost-Pieter (2000) On the Use of Model Checking Techniques for Quantitative Dependability Evaluation. In: 19th IEEE Symposium on Reliable Distributed Systems, SRDS 2000, 16-18 October 2000, Nürnberg, Germany (pp. pp. 228-237).

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract:Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras, or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.
Item Type:Conference or Workshop Item
Copyright:© 2000 IEEE
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/63278
Official URL:https://doi.org/10.1109/RELDI.2000.885410
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page