A Junction between State Based and Behavioural Specification

Two of the dominant paradigms for formally describing and analysing OO distributed systems are state based specification, e.g. Object-Z, and behavioural specification, e.g. process algebra. The style of specification embodied by the two paradigms is highly contrasting. With state based techniques the data state is explicitly defined while the temporal ordering of operations is left implicit, in contrast in behavioural techniques, no explicit data state definition is given while the temporal ordering of action offers is focused on. However, in order to support sophisticated software engineering principles, e.g. multi-paradigm specification, viewpoints modelling and subtyping, there is now considerable interest in developing strategies for relating state based and behavioural specification paradigms. This paper serves two purposes - firstly, it reviews the existing body of work on relating these two specification paradigms and secondly, it presents some new results on the topic. In particular, we present a testing characterisation of downward simulation, which is the standard state based refinement relation and is also closely related to subtyping. Central to this characterisation is giving a behavioural interpretation to the meaning of state based operations outside their pre-conditions