Relational Concurrent Refinement - partial and total frameworks

Derrick, John and Boiten, Eerke Albert (2016) Relational Concurrent Refinement - partial and total frameworks. In: Petre, Luigia and Sekerinski, Emil, eds. From Action Systems to Distributed Systems: The Refinement Approach. Taylor and Francis, Florida, USA, pp. 143-154. ISBN 9781498701587. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)

Abstract

Data refinement as found in a state-based language such as Z or B, and refinement as defined in a process algebra may appear as very different notions. Data refinement is defined using a relational model in terms of the behaviour of abstract programs, whereas in models of concurrency, refinement is often defined in terms of sets of observations. The methodologies used to verify them are also different: downward and upward simulations for data-refinement, whereas calculation of traces, refusals etc from the semantics is prevalent in a process algebra. In this chapter we discuss work undertaken to reconcile the two approaches. Specifically, we show how one can embed concurrent semantics into a relational framework. This not only articulates the relationship between the two, but allows event-wise verification methods for concurrent refinement relations to be derived. We discuss how this can be achieved, with particular emphasis on the type of relational model used - specifically whether one uses a model containing total relations, or one in which relations may be partial. Both are shown to have limits in expressiveness, and because of this we introduce a more general framework for simulations, called process data types.

Item Type: Book section
Uncontrolled keywords: refinement, process algebra, state-based systems, concurrency, simulation
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, > QA76.76 Computer software
Divisions: Faculties > University wide - Teaching/Research Groups > Centre for Cyber Security Research
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: E.A. Boiten
Date Deposited: 10 Nov 2015 00:50 UTC
Last Modified: 26 Jan 2017 14:19 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/51618 (The current URI for this page, for reference purposes)
Boiten, Eerke Albert: https://orcid.org/0000-0002-9184-8968
  • Depositors only (login required):