12th Asia-Pacific Software Engineering Conference (APSEC'05)
An Alternative Approach to Handling Nondeterminism in Model-Oriented Data-Refinement
Taipei, Taiwan
December 15-December 17
ISBN: 0-7695-2465-6
This paper investigates data-refinement by forward and backward simulations for model-oriented specifications whose semantics is given by partial relations. The most well-known example of such a semantics is that for Z. The standard model-theoretic characterisation of refinement is a relational approach based on totalisation and lifting. We contrast this, and relate it to, a new approach inspired by various concepts in algebraic paradigms and Type Theory (adapted into a framework based on classical logic) for handling nondeterminism and underspecification in datarefinement. We provide a new characterisation of refinement based on extracting a set of (deterministic) "implementations", each of which models the specification in question. We examine a means by which data simulations interact with this notion and demonstrate that each of the ensuing simulation-based theories is equivalent to the corresponding standard relational characterisation of refinement.
Citation:
Moshe Deutsch, Martin C. Henson, "An Alternative Approach to Handling Nondeterminism in Model-Oriented Data-Refinement," apsec, pp.149-158, 12th Asia-Pacific Software Engineering Conference (APSEC'05), 2005