About Performance Evaluation Process Algebra
Despite impressive improvements in the computational power which is
now available to end-users of computer systems, computer equipment is
still expensive to purchase and maintain. Consequently, making
cost-effective use of limited resources remains one of the motivating
concerns of developers of computer-controlled systems from flexible
manufacturing systems to high-availability databases. The analysis of
computer systems through construction and solution of descriptive
models is a hugely profitable activity: brief analysis of a model can
provide as much insight as hours of simulation and measurement.
Simple models of a computer system can be constructed without any explicit notational support. However, as computer systems become more complex so do their models and the use of a high-level language to aid in their expression becomes necessary. Jane Hillston's Performance Evaluation Process Algebra (PEPA) is an expressive formal language for modelling distributed systems. PEPA models are constructed by the composition of components which perform individual activities or cooperate on shared ones. To each activity is attached an estimate of the rate at which it may be performed. Using such a model, a system designer can determine whether a candidate design meets both the behavioural and the temporal requirements demanded of it.
A stochastic process algebra such as PEPA offers several attractive features which were not available in previous performance modelling paradigms. The most important of these are:
- compositionality, the ability to model a system as the interaction of subsystems,
- formality, giving a precise meaning to all terms in the language, and
- abstraction, the ability to build up complex models from detailed components, disregarding the details when it is appropriate to do so.
Queueing networks offer compositionality but not formality; stochastic extensions of Petri nets offer formality but not compositionality; neither offer abstraction mechanisms.
Performance modelling with PEPA
PEPA models contain information about the duration of activities and, via a race policy, their relative probabilities. From these models it is possible to generate a corresponding continuous time Markov chain (CTMC) by elaborating the model against the structured operational semantics of the PEPA language. Linear algebra can then be used to solve the model in terms of equilibrium behaviour. This behaviour is represented as a probability distribution over all the possible states of the model. This distribution is seldom the ultimate goal of performance analysis; instead the modeller is interested in performance measures which must be derived from this distribution via a reward structure defined over the CTMC.
The PEPA language is supported by a range of tools developed by its users round the world. The leading PEPA tool is the PEPA Eclipse Plug-in (download) which has been adopted by several groups of external users. The application areas for this work span the subject areas of Informatics and engineering.
- Active badge systems (Clark, Gilmore and Hillston, Edinburgh)
- Cellular telephone networks (Kloul, Versailles)
- Database systems (The STEADY group, Heriot-Watt and Clark, Edinburgh)
- Diagnostic expert systems (Ribaudo, Turin)
- Elevator systems (Kwiatkowska, Birmingham)
- Multimedia traffic characteristics (Bowman, UKC)
- Multiprocessor access-contention protocols (Gilmore, Hillston and Ribaudo)
- Multi-server, multi-queue systems (Harrison, Imperial and Hillston, Edinburgh)
- On-line auction systems (Hillston, Edinburgh and Kloul, Versailles)
- Protocols for fault-tolerant systems (Clark, Gilmore, Hillston and Ribaudo)
- Robotic workcells (Holton, Bradford and Gilmore and Hillston, Edinburgh)
- Software architectures (Pooley, Heriot-Watt and Thomas and Bradley, Durham)
- System-on-chip technology (Eder, Bristol)
More recently support for the PEPA language has been added to other tools such as the Mobius Modeling Framework (screenshot) from the Performability Engineering Research Group, Motorola Center for High-Availability System Validation at the University of Illinois at Urbana-Champaign. PEPA is also supported by the PRISM probabilistic model checker (screenshot) from the University of Birmingham, England. PEPA support is also built in to the Caesar/Aldebaran Development Package (screenshot) from the VASY group, INRIA Rhone-Alpes.
History of the PEPA project
Jane Hillston defined the PEPA language in her PhD thesis, undertaken in the Laboratory for Foundations of Computer Science, a research institute of the Division of Informatics. Her PhD thesis was awarded the British Computer Society/Conference of Professors and Heads of Computing Distinguished Dissertation award in 1995 and is published by Cambridge University Press. In 2004 Jane won the BCS/Microsoft Roger Needham award for her work on PEPA and compositional approaches to performance modelling. In May 2005 Jane was awarded a five-year Advanced Research Fellowship from the Engineering and Physical Sciences Research Council to support her research on quantified methods and process algebras.