Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Performance Evaluation:= (Process Algebra + Model Checking) X Markov Chains
| |
|
Performance Evaluation:= (Process Algebra + Model Checking) X Markov Chains
Holger Hermanns6 and Joost-Pieter Katoen6
| (6) |
Formal Methods and Tools Group Faculty of Computer Science, University of Twente, P.O. Box 217, 7500 AE Enschede, The Netherlands |
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.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|