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. (Contact us about this Publication)
Official URL


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: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01 UTC
Last Modified: 30 Aug 2019 11:44 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):