View article

Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. We 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₁ to a higher-level one S₂ is a mapping from S₁'s state space to S₂'s state space. It maps steps of S₁'s state machine to steps of S₂'s state machine and maps behaviors allowed by S₁ to behaviors allowed by S₂. We show that, under reasonable assumptions about the specification, if S₁ implements S₂, then by adding auxiliary variables to S₁ we can guarantee the existence of a refinement mapping. This provides a completeness result for a practical, hierarchical specification method.