|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: [email protected] |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page