Modelling divergence in Relational Concurrent Refinement

Boiten, E.A. and Derrick, J. (2009) Modelling divergence in Relational Concurrent Refinement. In: IFM 2009: Integrated Formal Methods. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1007/978-3-642-00255-7

Abstract

Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements. On the other hand, refinement in a process algebra takes a number of different forms depending on the exact notion of observation chosen, which can include the events a system is prepared to accept or refuse. In this paper we investigate how divergence can be modelled relationally, and in particular show how differing process algebraic interpretations of divergence can be embedded in a relational framework. In doing so we derive relational simulation conditions for process algebraic refinement incorporating divergence.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Data refinement, simulations, internal operations, process algebraic refinement preorders, divergence
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: 29 Mar 2010 12:11
Last Modified: 29 Mar 2010 12:11
Resource URI: http://kar.kent.ac.uk/id/eprint/24032 (The current URI for this page, for reference purposes)
  • Depositors only (login required):