Lehrstuhl fur Informatik (Erlangen, Germany)
CADP (Construction and Analysis of Distributed Processes)
TIPPtool (Timed Processes and Performance evaluation)
more than 1,000 lines of LOTOS
This case-study involves the performance analysis of a plain-old telephony system (POTS) using a non-traditional performance technique. Starting from a description of the POTS in LOTOS extended with time constraints, a continuous-time Markov chain is generated and minimised using the techniques available for process algebras.
The stochastic time constraints are specified by extending Basic LOTOS with a time-prefix operator. The semantics of the resulting stochastic process algebra is an orthogonal extension of the standard LOTOS semantics and of (homogeneous) continuous-time Markov chains. In order to facilitate the specification of phase-type durations, an auxiliary elapse operator is also introduced.
Starting from the LOTOS specification of the POTS, a highly irregular Markov chain of 720 states is generated. This Markov chain is subsequently used to carry out a transient performance analysis of the POTS.
Since the LOTOS specification has more than 10 million states, it could not be handled directly, but component-wisely by decomposing the system and applying CADP and the TIPPtool in a compositional way.
The model-checking verification technology available for process algebras and languages like LOTOS are particularly useful also for carrying out performance analysis of systems. In particular, LOTOS can be extended in a simple and modular way with stochastic operators, and the compositional generation features of the CADP toolset can be used in the context of Markov chain generation and minimisation.
Holger Hermanns and Joost-Pieter Katoen.
Automated Compositional Markov Chain Generation for a
Plain-Old Telephone System,
Science of Computer Programming, 1998.
University of Twente
Dept. of Computer Science
P.O. Box 217
NL-7500 AE Enschede
Tel: +31 53 4 893 755
Fax: +31 53 4 893 247
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|