Relating Behavioural and State Based Specification Techniques

Howard Bowman

My main collaborator on this topic has been John Derrick, however, Eerke Boiten, Charles Briscoe-Smith, Maarten Steen and Ben Strulo have also been involved.

Two of the dominant paradigms for formally describing and analysing computational systems are state based specification, e.g. Z and behavioural specification, e.g. process algebras, such as LOTOS. The style of specification embodied by the two is without doubt highly contrasting:-

• With State Based Techniques the data state is described explicitly, e.g. via Z state schemas. Then operations are defined over this state space, with the pre-condition of the operation defining the data states at which an operation can be applied and the post-condition defining the data results of applying an operation. Thus, the temporal order of operations is not explicitly defined.

• In contrast, with Behavioural Techniques no explicit definition of the data state is given, rather the specification comprises an expression of the temporal order in which events can occur.

However, despite these differences, it turns out that the two paradigms can be related, the key to which is to give a behavioural interpretation to state based specifications. For example, assuming a states and operations interpretation, Z can be mapped to a transition system (or even a failures semantics). This then gives a common semantics for process algebra and state based techniques from which the two paradigms can be related.

Building upon such behavioural interpretations of Z we have investigated two issues:

• Translation. How to translate process algebras into state based notations in a manner which preserves observational equivlance. This work has been performed within the bounds of the Cross Viewpoint Consistency in Open Distributed Process Project.

• Relating Preorders. How do preorders in the different notations relate to one another? In particular, on first sight the standard state based preorders, e.g. Z refinement, seem very different from the standard process algebra preorders, e.g. the LOTOS reduction relation or CSP's failures-divergences refinement. However, in the following paper we discuss how the different notions can be related and reconciled:-

  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.

Back to Howard Bowman's home page.

Last modified December 1999.