We introduce Performance Trees, a novel representation formalism for the specification of model-based performance queries. Traditionally, stochastic logics have been the prevalent means of performance requirement expression; however, in practice, their use amongst system designers is limited on account of their inherent complexity and restricted expressive power. Performance Trees are a more accessible alternative, in which performance queries are represented by hierarchical tree structures. This allows for the convenient visual composition of complex performance questions, and enables not only the verification of stochastic requirements, but also the direct extraction of performance measures. In addition, Performance Trees offer a superset of the expressiveness of Continuous Stochastic Logic (CSL) since all CSL formulae can be translated into our representation.
Performance Trees can be used to represent passage time, transient, steady-state and higher order queries of varying levels of sophistication. While they are conceptually independent of the underlying stochastic modelling formalism, in many cases the tree operators we use are already backed up by good algorithmic and tool support for both stochastic verification and performance measure extraction. We do not therefore perceive major barriers to the integration of Performance Trees into existing stochastic model checking tools. Indeed, we illustrate how semi-Markov passage time computation algorithms, based on numerical Laplace transform inversion, can be directly applied to the resolution of a case study Performance Tree query.
Information from pubs.doc.ic.ac.uk/performance-trees.