Retrenchment, Refinement, and Simulation

: Retrenchment is introduced as a liberalisation of refinement intended to address some of the shortcomings of refinement as sole means of progressing from simple abstract models to more complex and realistic ones. In retrenchment the reip between an abstract operation and its concrete counterpart is mediated by extra predicates, allowing the expression of non-refinement-like properties and ng of I/O and state aspects in the passage between levels of abstraction. Modulated refinement is introduced as a version of refinement allowing mixing of I/O and state aspects, in order to facilitate comparison between retrenchment and refinement, and various notions of simulation are considered in this context. Stepwise simulation, the ability of the simulator to mimic a sequence of execution steps of the simulatee in a sequence of equal length is proposed as the benchmark semantic notion for relating concepts in this area. One version of modulated refinement is shown to have particularly strong c...

• Type: Conference
• Year: 2000
• Where: ZUM
• Authors: Richard Banach, Michael Poppleton
• Keywords: Formal Methods, Refinement Allowing Mixing, Retrenchment, State Aspects, ZUM 2000