Formal Methods for Real-time, Multimedia and Stochastic Systems

Howard Bowman

The "first generation" of formal methods, e.g. CCS, CSP, LOTOS, temporal logics, petri nets etc, did not support specification of real-time aspects. They allowed description and verification of "event ordering", i.e. the allowed order in which events can occur. For example, they would enable the possible orderings of sending, receiveing and acknowledging in a data link protocol to be described and then enable deadlock and livelock freeness of the description to be verified. Nearly all the notations developed abstracted from real-time aspects; put another way, they allowed the qualitative, but not the quantitative ordering of events to be defined.

However, there are now a large variety of systems for which real-time is a central aspect and descriptions which ignore it are insufficient. Consequently, and along with a number of other researchers, I have been working on extending "first generation" formal methods with features to describe and analysis real-time properties of systems.

My work on this topic can be placed under a number of headings:-

I consider these topics in turn.

Timed Process Algebra

Process algebra are one of the most successful notations for describing concurrent systems. The basic concepts of the approach were conceived by Robin Milner and Tony Hoare in their respective approaches CCS (see, e.g. The Concurrency Factory Tool) and CSP. However, since their initial work, a large number of process algebra approaches have been developed, including LOTOS, which has been the subject of my work. I have made a number of contributions to the issue of how to add real-time to LOTOS.

I first worked on a very simple approach to adding real-time to process algebra, in which the quantitative aspects are separated from the qualitative aspects. The resulting approach combines real-time temporal logic with LOTOS:

Time versus abstraction in formal description. H. Bowman, G.S. Blair, L. Blair, and A.G. Chetwynd. In Richard Tenney, Paul D. Amer, and Umit Uyar, editors, IFIP Transactions C_22, Proceedings of FORTE`93, Sixth International Conference on Formal Description Techniques, pages 467-482. North-Holland, October 1993.

More recently I have worked on how to give true concurrency semantics to time extended LOTOS calculi. The following two papers concern this topic. In particular, the second paper gives a true concurrency semantics to the important calculus, ET-LOTOS, which was the basis of the extended LOTOS standard.

Extending LOTOS with time: A True concurrency perspective. Howard Bowman and John Derrick. In Miquel Bertran and Teodor Rus, editors, ARTS'97, AMAST Workshop on Real-Time Systems, Concurrent and Distributed Software, volume 1231 of Lecture Notes in Computer Science, pages 382-399. Springer-Verlag, May 1997.

A true concurrency semantics for ET-LOTOS. Howard Bowman and Joost-Pieter Katoen. In CSD'98 International Conference on Application of Concurrency to System Design, IEEE Computer Society. IEEE Computer Society Press, March 1998.

The text and an extended version of this last paper can be found on Joost-Pieter Katoen's publication page.

Timed Automata and Timelocks

In many of the existing timed specification notations, e.g. Timed Process Algebra and Timed Automata, timelocks can freely arise. These are situations in which time is prevented from passing beyond a certain point. They are highly degenerate occurrences because they yield a global blockage of the systems evolution. In particular, if a completely independent component is composed in parallel with a system that is timelocked, then the entire composition will inherit the timelock. This is quite different from a classic action based deadlock, which cannot affect the evolution of an independent process.

Timelocks can typically arise for two main reasons:

Zeno Behaviour. In many timed specification notations it is possible to describe repetitive behaviour in which an infinite number of events can occur in a finite period of time. Such behaviour is typically called zeno as it ostensibly corresponds to the zeno paradox over the real numbers which was observed by Zeno of Elea in the fifth century B.C..
Synchronisation. Perhaps most problematically timelocks can arise through the interplay of inter-process synchronisation (/communication) and strong timing constraints (i.e. urgency).

Furthermore, given an arbitrary timed specification, due to state explosion problems, it is difficult to determine that the specification is timelock free through automatic analysis. For this and a number of other reasons I have worked on revising timed specification notations in order to prevent the occurence of timelocks.

My first work on this topic was in a timed process algebra setting. Specifically, due to the particular manner in which urgency was enforced, the true concurrency approach to time extended LOTOS that I worked on allows timelocks in fewer situations than the standard interleaved approach. The following paper is the most complete publication of this approach:

A true concurrency semantics for ET-LOTOS. Howard Bowman and Joost-Pieter Katoen. In CSD'98 International Conference on Application of Concurrency to System Design, IEEE Computer Society. IEEE Computer Society Press, March 1998.

Also, as highlighted earlier, the text and an extended version of this paper can be found on Joost-Pieter Katoen's publication page.

Then I considered the timelock problem in a timed automata setting. In particular, the following paper highlights the difficults that timelocks can cause. It presents a timed automata based specification and analysis of a lip-synchronisation algorithm, in which, many timelock situations arise. The (model checking) analysis technique that was used was UPPAAL.

Automatic verification of a lip synchronisation protocol using UPPAAL. H. Bowman, G. Faconti, J.-P. Katoen, D. Latella, and M. Massink. Formal Aspects of Computing, page 26, April 1999. Special Issue on Formal Methods for Industrial Critical Systems.

In response to the problems that timelocks caused in the analysis of the lip-sync algorithm, I have considered re-definitions of timed automata parallel composition in order to avoid the possibility of timelocks arising through mis-matched synchronisations. This work was strongly influenced by the Timed Automata with Deadlines approach of Sebastian Bornot and Joseph Sifakis.

My work on this topic was reported in the paper:

Modelling timeouts without timelocks. Howard Bowman. In ARTS'99, 5th International AMAST Workshop on Real-time and Probabilistic Systems, Lecture Notes in Computer Science, page 20. Springer-Verlag, May 1999.

Verification of Distributed Multimedia Systems

I have also worked extensively on the problem of how to specify and verification distributed multimedia systems.

My initial work on this topic focused on the problem of specifying distributed multimedia systems and was most extensively reported in the book,

Formal specification of distributed multimedia systems. G.S. Blair, L. Blair, H. Bowman, and A. Chetwynd. University College London Press, September 1997.

However, I have more recently been working on the problem of verifying distributed multimedia systems. This amounts to verifying that a description of a system satisfies certain quality of service properties such as latency, throughput and jitter. The following two papers show how timed model checking can be used in such a verification scenario. In both cases, the timed model checher used was UPPAAL.

Specification and verification of media constraints using UPPAAL. H. Bowman, G. Faconti, and M. Massink. In 5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, DSV-IS 98, Eurographics Series. Springer-Verlag, August 1998.

Automatic verification of a lip synchronisation protocol using UPPAAL. H. Bowman, G. Faconti, J.-P. Katoen, D. Latella, and M. Massink. Formal Aspects of Computing, page 26, April 1999. Special Issue on Formal Methods for Industrial Critical Systems.

A lot of my work on this topic has been performed within the bounds of the EPSRC funded V-QOS project.

Stochastic Analysis

An important area of current research is the integration of concurrency theory and performance modelling techniques. The features of the two techniques are complementary and their integration is beneficial for both fields:-

Performance Modelling techniques, such as queuing theory, will benefit from the richer behavioural specification properties of concurrency theory techniques. The most significant example of this is that notations from concurrency theory, such as process algebra or communicating automata, allow systems to be described component by component in a compositional fashion. Such specification flexibility is not typically supported by classic performance modelling techniques, which are largely flat in nature.
Concurrency Theory has strived to increase the class of systems that it can be used to describe. This can be clearly seen in the process algebra domain. First untimed calculi were developed. These calculi allow the order of event occurences to be defined. Then real-time calculi were considered, which allow event occurences to be related to the passage of quantitative deterministic time. At a similar point probabilistic approaches were considered. These allow probabilistic choices to be defined, rather than the simple non-deterministic choices of standard process calculi.
A natural next step is to consider stochastic calculi. These allow real-time delays to be selected according to particular probability distributions and also provide a form of probabilistic choice through the race condition on branching.

A number of research groups have made important contributions to this topic, e.g.

Jane Hillston's PEPA group at Edinburgh University.
Ulrich Herzog's group at the University of Erlangen.
Ed Brinksma and Joost-Pieter Katoen's group at the University of Twente.
Marta Kwiatkowska's group at Birmingham University.

Also, the PAPM workshop has been an important source of work on this topic.

My work in this area has been within the bounds of the V-QOS project. In particular, the following publication from this project considers how stochastic process algebra can be used to verify quality of service.

Analysis of a multimedia stream using stochastic process algebra. Howard Bowman, Jeremy Bryans, and John Derrick. In Corrado Priami, editor, Sixth International Workshop on Process Algebras and Performance Modelling, pages 51-69, Nice, September 1998.

Perhaps the most promising direction being considered in this field at the moment is stochastic model checking. In this approach the classic (concurrency theory) technique of model checking is enhanced to answer probabilistic and stochastic questions over continuous time markov chains. Perhaps the most mature work on this topic is that of the group at the University of Twente, see the publications on Holger Hermann's web page.

Within the V-QOS project, we are looking at model checking algorithms for models which allow generalised distributions rather than the exponential distributions arising in continuous time markov chains.

Specifying Multimedia Documents using Interval Temporal Logic

See this page.

Back to Howard Bowman's home page.

Last modified December 1999.