The existence of refinement mappings

Abstract

Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. The authors consider specifications consisting of a state machine (which may be infinite-state) that specifies safety requirements and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a lower-level specification S/sub 1/ to higher-level one S/sub 2/ is a mapping from S/sub 1/'s state space to S/sub 2/'s state space that maps steps of S/sub 1/'s state machine steps to steps of S/sub 2/'s state machine and maps behaviors allowed by S/sub 1/ to behaviors allowed by S/sub 2/. It is shown that under reasonable assumptions about the specifications, if S/sub 1/ implements S/sub 2/, then by adding auxiliary variables to S/sub 1/ one can guarantee the existence of a refinement mapping. This provides a completeness result for a practical hierarchical specification method.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>