Skip to main content

Using coupled simulations in non-atomic refinement

Derrick, John and Wehrheim, Heike (2003) Using coupled simulations in non-atomic refinement. In: Bert, Didier and Bowen, Jonathan P. and King, Steve and Walden, Marina, eds. ZB 2003: Formal Specification and Development in Z and B Third International Conference of B and Z Users. Lecture Notes in Computer Science . Springer, pp. 127-147. ISBN 978-3-540-40253-4. E-ISBN 978-3-540-44880-8. (doi:10.1007/3-540-44880-2_10) (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) (KAR id:13964)

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.
Official URL:
http://dx.doi.org/10.1007/3-540-44880-2_10

Abstract

Refinement is one of the most important techniques in formal system design, supporting stepwise development of systems from abstract specifications into more concrete implementations. Non-atomic refinement is employed when the level of granularity changes during a refinement step, i.e., whenever an abstract operation is refined into a sequence of concrete operations, as opposed to a single concrete operation. There has been some limited work on non-atomic refinement in Z, and the purpose of this paper is to extend this existing theory. In particular, we strengthen the proposed definition to exclude certain behaviours which only occur in the concrete specification but have no counterpart on the abstract level. To do this we use coupled simulations: the standard simulation relation is complemented by a second relation which guarantees the exclusion of undesired behaviour of the concrete system. These two relations have to agree at specific points (coupling condition), thus ensuring the desired close correspondence between abstract and concrete specification.

Item Type: Book section
DOI/Identification number: 10.1007/3-540-44880-2_10
Additional information: Conference Information: 3rd International Conference on B and Z Users. ClearSy Syst Engn; Nokia; BCS FACS; FME; Z User Grp
Uncontrolled keywords: Non-atomic refinement; action refinement; Z; coupled simulations
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: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/13964 (The current URI for this page, for reference purposes)

University of Kent Author Information

Derrick, John.

Creator's ORCID:
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.