Performance evaluation:= (process algebra + model checking) x Markov chains

Hermanns, H. and Katoen, J.P. (2001) Performance evaluation:= (process algebra + model checking) x Markov chains. In: 12th International Conference on Concurrency Theory, CONCUR 2001, 20-25 Aug 2001, Aalborg, Denmark.

Preview

PDF
257Kb

Abstract:	Markov chains are widely used in practice to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This tutorial paper shows how successful model specification and analysis techniques from concurrency theory can be applied to performance evaluation. The specification of CTMCs is supported by a stochastic process algebra, while the quantitative analysis of these models is tackled by means of model checking. Process algebra provides: (i) a high-level specification formalism for describing CTMCs in a precise, modular and constraint-oriented way, and (ii) means for the automated generation and aggregation of CTMCs. Temporal logic model checking provides: (i) a formalism to specify complex measures-of-interest in a lucid, compact and flexible way, (ii) automated means to quantify these measures over CTMCs, and (iii) automated measure-driven aggregation (lumping) of CTMCs. Combining process algebra and model checking constitutes a coherent framework for performance evaluation based on CTMCs.
Item Type:	Conference or Workshop Item
Copyright:	© 2001 Springer
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/66268
Official URL:	http://dx.doi.org/10.1007/3-540-44685-0_6
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page