Derrick, John, Boiten, Eerke Albert (1999) Calculating upward and downward simulations of state-based specifications. Information and Software Technology, 41 (13). pp. 917-923. ISSN 0950-5849. (doi:10.1016/S0950-5849(99)00044-0) (KAR id:17282)
PDF
Language: English |
|
Click to download this file (170kB)
|
![]() |
This file may not be suitable for users of assistive technology.
Request an accessible format
|
|
Postscript
Language: English |
|
Click to download this file (176kB)
Preview
|
Preview |
This file may not be suitable for users of assistive technology.
Request an accessible format
|
|
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 |
---|---|
DOI/Identification number: | 10.1016/S0950-5849(99)00044-0 |
Uncontrolled keywords: | refinement; state-based systems; Z; calculating refinements |
Subjects: | Q Science |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Eerke Boiten |
Date Deposited: | 14 Jun 2009 19:25 UTC |
Last Modified: | 16 Nov 2021 09:55 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/17282 (The current URI for this page, for reference purposes) |
Boiten, Eerke Albert: |
![]() |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):