An Analysis of Backward Simulation Data-Refinement for Partial Relation Semantics

This paper investigates data-refinement by backward simulation for specifications whose semantics is given by partial relations. The standard model-theoretic approach is based on totalisation and lifting. The paper examines this model, exploring and isolating the precise roles played by lifting and totalisation in the standard account by introducing a simpler, normative theory of backward simulation data-refinement (SB-refinement) which captures refinement directly in the language and in terms of the natural properties of preconditions and postconditions. This theory is used in conjunction with four other model-theoretic approaches to determine the extent to which the standard approach is canonical, and the extent to which it is arbitrary.

• Type: Conference
• Year: 2003
• Where: APSEC
• Authors: Moshe Deutsch, Martin C. Henson
• Keywords: APSEC 2003, Backward Simulation, Paper Investigates Data-refinement, Software Engineering, Standard Model-theoretic Approach