Derrick, J. and Wehrheim, H. (2003) Using coupled simulations in non-atomic refinement. In: ZB 2003: Formal Specification and Development in Z and B, Jun 04-06, 2003, Turku, Finland, .
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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:||Conference or workshop item (UNSPECIFIED)|
|Additional information:||Conference Information: 3rd International Conference on B and Z Users. ClearSy Syst Engn; Nokia; BCS FACS; FME; Z User Grp|
|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:||24 Nov 2008 18:01|
|Last Modified:||12 Jun 2012 12:58|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/13964 (The current URI for this page, for reference purposes)|
- Depositors only (login required):