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 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.
Timelocks can typically arise for two main reasons:
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.
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.
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.
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.
Back to Howard Bowman's home page.
Last modified December 1999.