Calculating upward and downward simulations of state-based specifications

Derrick, J. and Boiten, E.A. (1999) Calculating upward and downward simulations of state-based specifications. Information and Software Technology, 41 (13). pp. 917-923. ISSN 0950-5849. (Full text available)

PDF
Download (170kB)
[img]
Preview
Postscript
Download (176kB)
[img]
Preview
Official URL
http://dx.doi.org/10.1016/S0950-5849(99)00044-0

Abstract

This paper concerns calculational methods of refinement in state-based specification languages. Data refinement is a well-established technique for transforming specifications of abstract data types into ones, which are closer to an eventual implementation. The conditions under which a transformation is a correct refinement are encapsulated into two simulation rules: downward and upward simulations. One approach for refining an abstract system is to specify the concrete data type, and then attempt to verify that it is a valid refinement of the abstract type. An alternative approach is to calculate the concrete specification based upon the abstract specification and a retrieve relation, which links the abstract and concrete states. In this paper we generalise existing calculational methods for downward simulations and derive similar results for upward simulations; we also document their use and application in a particular specification language, namely Z.

Item Type: Article
Uncontrolled keywords: refinement; state-based systems; Z; calculating refinements
Subjects: Q Science
Divisions: Faculties > Science Technology and Medical Studies > School of Computing
Depositing User: M. Nasiriavanaki
Date Deposited: 14 Jun 2009 19:25
Last Modified: 06 Sep 2011 02:19
Resource URI: http://kar.kent.ac.uk/id/eprint/17282 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year