The Tempo II Project:
Specification and Validation of Quality of Service in Open Distributed Processing
Contents
Project undertaken at:
Computing Department, Lancaster University, Bailrigg, Lancaster, LA1 4YR
Dates: August 1994 - July 1996.
Participants of Tempo II were:
Abderrahmane Lakas
Neil Barnes
The aims of the Tempo II project were:
to develop the necessary formal techniques and tools for the specification and validation of real-time quality of service (QoS) properties in Open Distributed Processing (ODP), and
to integrate these formal techniques into the existing ODP framework.
The project built on previous research at Lancaster carried out in the Tempo project. This provided a strong foundation for Tempo II. However, there were a number of limitations with this initial research, namely:
the logic used in Tempo (QTL) was undecidable,
the full range of QoS properties were not supported (e.g. probabilistic properties), and
there was limited tool support for the specification approach developed.
These issues were addressed in Tempo II.
The project initially considered support for quality of service, drawing on related research at Lancaster from the Quality of Service Architecture project. Various QoS dimensions were identified which should be supported by the chosen formal specification technique, namely timeliness dimensions (including measurements of latency and jitter), volume dimensions (including measurements of throughput) and reliability dimensions (including measurement of percentage packet loss or bit error rates). For each of these dimensions, various types of property can be expressed:
deterministic properties - expressed in terms of the precise value or range of values required (e.g. throughput is between 20 and 25 frames per second)
probabilistic properties - expressed in terms of the probability of a particular target being achieved (e.g. the probability of receiving a video frame within 50ms is 0.9)
stochastic properties - expressing that a set of events should conform to a particular stochastic distribution (e.g. the inter-arrival times of video frames follows an exponential distribution with mean 40ms)
The overall approach developed under Tempo for the specification of distributed multimedia systems was a dual-language approach some and based on the principle of maintaining a separation of concerns. The methodology involved partitioning a system into functional and non-functional (time-critical) components.
As in the Tempo project, LOTOS was used for the specification of the functional behaviour of the system (called abstract behaviour). To specify the time-critical properties within the system (called real-time assumptions) a probabilistic and stochastic extension to QTL was developed, called SQTL. The abstract behaviour and the real-time assumptions together specify the behaviour of the system. The global model shown in the diagram above uses the novel concept of event schedulers. These are timed and probabilistic automaton-based models, which can be used to schedule events in the abstract behaviour. In terms of LOTOS, every action which is enabled in the underlying labelled transition system is submitted to the event scheduler which will decide, according to the timing information, if the action should occur and, if so, precisely when it should happen.
The logic SQTL may also be used to specify requirements over the system. The SQTL formulae can themselves be translated into event schedulers and verification techniques, developed for this approach, can be used. If only the probabilistic extensions to QTL are used, then symbolic model checking based on Alur's region based graphs can be used. Otherwise, if stochastic extensions are used, then we resort to a non-exhaustive technique which performs simulation on the composite behaviour.
Prototype tools have been developed to (i) generate event schedulers from SQTL formulae and (ii) simulating event schedulers. Some work was also carried out on composing event schedulers with LOTOS specifications and implementing the probabilistic model checking technique for SQTL. However, these were not completed at the end of the project.
A. Lakas, G. S. Blair and A. Chetwynd. A Formal Approach to the Design of QoS Parameters in Multimedia Systems. Proceedings of the 4th International Workshop on Quality of Service, Paris, France, March 1996.
A. Lakas, G. S. Blair and A. Chetwynd. Specification and Verification of Real-Time Properties Using LOTOS and SQTL. Proceedings of the 8th International Workshop on Software Specification and Design, Paderborn, Germany, March 1996.
A. Lakas, G. S. Blair and A. Chetwynd. Specification of Stochastic Properties in Real-Time Systems. Proceedings of the 11th UK Performance Engineering Workshop for Computer and Telecommunications Systems (Liverpool, Sept. 1995), M. Merabti, M. Carew, F. Ball (eds), pp 202-216, Springer-Verlag, 1996.
N. Barnes, G. S. Blair, A. Lakas and A. Chetwynd. Costing-Extending the Locative Logic Model of Networks. Proceedings of the 8th EuroMicro Workshop on Real-Time Systems, L'Aquila, Italy, June 1996.
Further information on other related projects can be found in:
Any comments/questions on this page to: lb@comp.lancs.ac.uk
Last change: January 1998 (L.B.)