Bowman, H. and Derrick, J. (1999) A Junction between State Based and Behavioural Specification. In: Formal Methods for Open Object-based Distributed Systems.
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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.
|Item Type:||Conference or workshop item (Paper)|
|Additional information:||Invited Paper|
|Uncontrolled keywords:||State based specification, process algebra, Z, Object-Z, LOTOS|
|Subjects:||Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,|
|Divisions:||Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group|
|Depositing User:||Mark Wheadon|
|Date Deposited:||20 Oct 2009 18:26|
|Last Modified:||20 Oct 2009 18:26|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/21871 (The current URI for this page, for reference purposes)|
- Depositors only (login required):