Compositional modelling, compact representation and analysis of performability propertiesMarkus Siegle (siegle@informatik.uni-erlangen.de)
Stochastic models have a long tradition in the areas of performance and dependability evaluation. Since their specification at a low level (e.g. that of a Markov chain) is tedious and error-prone, several high-level model specification formalisms have been developed, such as queueing networks, stochastic Petri nets and networks of stochastic automata, which allow humans to describe the intended behaviour at a convenient level of abstraction. Although - at least under Markovian assumptions - the analysis of the underlying stochastic process does not pose any conceptual problems, the size of the underlying state space often renders models intractable in practice. Structuring concepts, which were originally introduced at the Markov chain level, have shown to be of great value in order to alleviate this well-known state space explosion problem. A process algebra is a mathematically founded specification formalism which provides compositional features, such as parallel composition of components, abstraction from internal actions, and the replacing of components by behaviourally equivalent ones. Therefore, stochastic extensions of process algebras are among the methods of choice for constructing complex, hierarchically structured stochastic models. Recently, decision diagrams, which were originally developed as memory- efficient representations of Boolean functions in the area of hardware verification, have been extended in order to capture the numerical information which is contained in stochastic models. They have already been successfully used as the underlying data structure in prototype tools for performance analysis and verification of probabilistic systems. In this talk it is shown that symbolic representations based on decision diagrams are particularly attractive if applied in a compositional context, as provided, for example, by a process algebraic specification formalism. In many cases, decision diagrams allow extremely compact representations of huge state spaces, and it has been demonstrated that all steps of model construction, manipulation and analysis (be it model checking, numerical analysis, or a combination of the two) can be carried out efficiently on the decision diagram based representations. Thus, we argue that decision diagrams fit in ideally with structured modelling formalisms and open new ways towards increasing the range of manageable performance evaluation and verification problems. |