Derrick, J. and Boiten, E.A. (1999) Non-atomic refinement in Z. In: Wing, J.M. and Woodchck, J. and Davies, J., eds. FM’99 — Formal Methods. Lecture Notes In Computer Science, 1709 . Springer-Verlag Berlin, Berlin, Germany pp. 1477-1496. ISBN 978-3-540-66588-5.
| The full text of this publication is not available from this repository. (Contact us about this Publication) | |
| Official URL http://dx.doi.org/10.1007/3-540-48118-4_28 |
Abstract
This paper discusses the refinement of systems specified in Z when we relax the assumption that the refinement will preserve the atomicity of operations. Data refinement is a well established technique for transforming specifications of abstract data types into ones which are closer to an eventual implementation. To verify a refinement a retrieve relation is used which relates the concrete to abstract states and allow the comparison between the data types to be made on a step by step basis by comparing an abstract operation with its concrete counterpart. A step by step comparison is possible because the two abstract data types are assumed to be conformal, i.e. there is a one-one correspondence between abstract and concrete operations, so each abstract operation has a concrete counterpart. In this paper we relax that assumption to discuss refinements where an abstract operation is refined by, not one: but a sequence of concrete operations. Such non-conformal or non-atomic refinements arise naturally in a number of settings and we illustrate our derivations with a simple example of a bank accounting system.
| Item Type: | Conference or workshop item (Paper) |
|---|---|
| Additional information: | Conference Information: Event title: 1st World Congress on Formal Methods in the Development of Computing Systems (FM 99); Event location: Toulouse, France; Event dates: Sep 20-24, 1999; AMAST; Aerospatiale Airbus; Alcatel Space; CCIT; CEPIS; CNES; CNRS; Cap Gemimi; Carnegie Mellon Univ; Conseil Reg Midi Pyrenees; DGA; EATCS; ESA; ETAPS; European Union; FACS; FME; France Telecom; IFIP; INRIA; IPSJ; IRIT; JSSST; LAAS; Mairie Toulouse; Matra Marconi Space; ONERA; Tech Univ Delft; Tech Univ Denmark; Tech Univ Graz; Translimina; Univ Oxford; Univ Reading |
| Uncontrolled keywords: | specification; refinement; Z; non-atomic refinement; non-atomic operations |
| Subjects: | Q Science Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Faculties > Science Technology and Medical Studies > School of Computing |
| Depositing User: | M. Nasiriavanaki |
| Date Deposited: | 14 Jun 2009 19:40 |
| Last Modified: | 06 Oct 2009 15:45 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/17280 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
