Performance analysis and true concurrency semantics

This paper addresses the subject of linking functional specifications to performance analysis in a process algebraic context. It presents a timed, probabilistic extension of a process algebraic formalism and its application to performance analysis. More specifically, an extension of a subset of LOTOS is presented equipped with a truly concurrent semantical model based on bundle event structures. It is investigated how semi-Markov chains can be obtained from functional speciications using this semantical model. The use of a true concurrency model enables us to distinguish between non-determinism and parallelism, to reduce the state explosion problem and, moreover, to analyse part of the system wi thout considering other (irrelevant) parts. An example illustrates the proposed approach.