Relating Behavioural and State Based Specification Techniques

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:-

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:

Other links that consider related issues include our discussion of type management in distributed systems and Eerke Boiten and John Derrick's page on state based refinement.

Back to Howard Bowman's home page.

Last modified December 1999.