Performance Prediction of Behavioural Descriptions with Temporal Logics (Extended Abstract)

Stochastic Process Algebras (SPA) allow the integration of performance evaluation into early design phases of distributed systems. However, due to their behaviour oriented description, the definition of performance characteristics is difficult. In classical performance evaluation, these characteristics are usually defined in a state oriented manner, because the notion of state is an essential part of the concept of queueing networks, (generalized) stochastic Petri nets as well as stochastic automata networks. In this deliverable we will sketch some ideas to bridge the gap between state and behaviour oriented description by means of a simple temporal logic. This approach can be adapted to various existing behaviour oriented specification languages. Especially for LOTOS this bridge to classical performance evaluation is important, because the formal foundation of SPA can be extended to Basic-LOTOS straightforwardly. The QMIPS Project: The QMIPS project is a collaborative research projec..