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.
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):
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_postscript.png)
