Automated compositional Markov chain generation for a plain-old telephone system

Citation
H. Hermanns et Jp. Katoen, Automated compositional Markov chain generation for a plain-old telephone system, SCI COMP PR, 36(1), 2000, pp. 97-127
Citations number
42
Categorie Soggetti
Computer Science & Engineering
Journal title
SCIENCE OF COMPUTER PROGRAMMING
ISSN journal
01676423 → ACNP
Volume
36
Issue
1
Year of publication
2000
Pages
97 - 127
Database
ISI
SICI code
0167-6423(200001)36:1<97:ACMCGF>2.0.ZU;2-0
Abstract
Obtaining performance models, like Markov chains and queueing networks, for systems of significant complexity and magnitude is a difficult task that i s usually tackled using human intelligence and experience. This holds in pa rticular for performance models of a highly irregular nature. In this paper we argue by means of a non-trivial example - a plain-old telephone system (POTS) - that a stochastic extension of process algebra can diminish these problems by permitting an automatic generation of Markov chains. We introdu ce a stochastic process algebra that separates the advance of time and acti on occurrences. For the sake of specification convenience we incorporate an elapse operator that allows the modular description of time constraints wh ere delays are described by continuous phase-type distributions. Using this language we provide a formal specification of the POTS and show how a stoc hastic process of more than 10(7) states is automatically obtained from thi s system description. Finally, we aggregate this model compositionally usin g appropriate stochastic extensions of (strong and weak) bisimulation. As a result we obtain a highly irregular Markov chain of about 700 states in an automated way, which we use to carry out a transient performance analysis of the POTS. (C) 2000 Elsevier Science B.V. All rights reserved.