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)|
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|
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):