A research interest of mine is the design of formally based techniques that can be applied to the specification and verification of distributed systems. Modern distributed systems incorporate a number of elements which were not present in the early generations of distributed systems, e.g. object based modelling, mobile processes, viewpoints modelling, multimedia, quality of service and real-time in general. Developing fully expressive formal models for these aspects is a significant research task.
I have worked with a number of people, including Lynne Blair, Gordon Blair, Eerke Boiten, Charles Briscoe-Smith, Jeremy Bryans, Amanda Chetwynd, John Derrick, Peter Linington, Maarten Steen and Ben Strulo, in addressing a number of these topics:-
The key issue that our work on this topic has considered is why is it that notions of refinement in process algebra, such as LOTOS's reduction relation, do not match the accepted intuition of behavioural subtyping in OO distributed systems. Intuitively speaking, behavioural subtyping should allow interface and (more broadly) trace extension. However, trace sets cannot be enlarged during process algebra refinement.
With reference to state based refinement from, e.g. Z, we have explained this aspect of process algebra refinement and we have considered ways to transform process algebra specifications in order to allow the required interface and trace extension.
The following paper considers our basic ideas on this topic:
On Behavioural Subtyping in LOTOS. H. Bowman, C. Briscoe-Smith, J. Derrick, and B. Strulo. In H. Bowman and J. Derrick, editors, FMOODS'97, Second IFIP International Conference on Formal Methods for Open Object-based Distributed Systems. Chapman and Hall, July 1997.However, some of our ideas have evolved since writing this paper and the most mature presentation of our ideas on this topic can be found in the following paper:
A junction between state based and behavioural specification. H. Bowman and J. Derrick. In A. Fantechi P. Ciancarini and R. Gorrieri, editors, Formal Methods for Open Object-based Distributed Systems, pages 213-239. Kluwer, February 1999. Invited Paper.Indeed this paper reflects our interest in relating state based and behavioural specification notations, which has grown out of our work on behavioural subtyping.
Charles Briscoe-Smith's PhD work was performed in this area and financial support for our work on this topic was provided by British Telecom.
In addition, I am currently involved in editing a book of collected articles on this topic, which will be published by Cambridge University Press.
Back to Howard Bowman's home page.
Last modified December 1999.