Database of Case Studies Achieved Using CADP

Plain Old Telephone System (POTS)

Organisation: Lehrstuhl fur Informatik (Erlangen, Germany)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)
TIPPtool (Timed Processes and Performance evaluation)

Domain: Telephony.

Period: 1998.

Size: more than 1,000 lines of LOTOS

Description: 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.

Conclusion: 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.

Publications: [Hermanns-Katoen-98] Holger Hermanns and Joost-Pieter Katoen. Automated Compositional Markov Chain Generation for a Plain-Old Telephone System, Bulletin of the EATCS

[Hermanns-Katoen-00] Holger Hermanns and Joost-Pieter Katoen. Automated Compositional Markov Chain Generation for a Plain-Old Telephone System, Science of Computer Programming, vol. 36(1), pages 97-127, 2000.

Contact:
Holger Hermanns
University of Twente
Dept. of Computer Science
P.O. Box 217
NL-7500 AE Enschede
The Netherlands
Tel: +31 53 4 893 755
Fax: +31 53 4 893 247
E-mail: hermanns@cs.utwente.nl



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Mon Oct 17 12:06:23 2022.


Back to the CADP case studies page