Skip to main content

Introducing extra operations in refinement

Boiten, Eerke Albert (2014) Introducing extra operations in refinement. Formal Aspects of Computing, 26 (2). pp. 305-317. ISSN 0934-5043. (doi:10.1007/s00165-012-0266-z) (KAR id:31991)

PDF (Version here is post-print. The final publication is available at link.springer.com. Available free while in "Online First" state.) Author's Accepted Manuscript
Language: English
Download this file
(PDF/315kB)
[thumbnail of Version here is post-print. The final publication is available at link.springer.com. Available free while in "Online First" state.]
Preview
Request a format suitable for use with assistive technology e.g. a screenreader
Official URL:
http://dx.doi.org/10.1007/s00165-012-0266-z

Abstract

This paper reconsiders refinements which introduce actions on the

concrete level which were not present at the abstract level. It considers a range of different

basic refinement relations, covering the standard ones for formalisms like Event-B, Z, action systems, and CSP.

It also describes a number of ways in which new operations may be introduced:

extended interfaces, internal actions, stuttering steps, and action refinement.

The main contribution of this paper is in exploring the interaction between those two dimensions. In particular, it shows how the "refining skip" method is incompatible with failures-based refinement relations, and consequently

some decisions in designing Event-B refinement are more entangled than previously highlighted.

Item Type: Article
DOI/Identification number: 10.1007/s00165-012-0266-z
Uncontrolled keywords: Refinement, action refinement, stuttering steps, ASM, Event-B, Z, internal operations, weak refinement, granularity, perspicuity, divergence.
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Eerke Boiten
Date Deposited: 26 Oct 2012 07:53 UTC
Last Modified: 16 Feb 2021 12:43 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/31991 (The current URI for this page, for reference purposes)

University of Kent Author Information

Boiten, Eerke Albert.

Creator's ORCID: https://orcid.org/0000-0002-9184-8968
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.