The existence of refinement mappings (Q805251)

A refinement mapping from a lower-level specification \(S_ 1\) to higher- level specification \(S_ 2\) can be used to prove that \(S_ 1\) is a correct implementation of \(S_ 2\)- if such a mapping does exist. The goal of the paper is to find out assumptions about specifications to guarantee the existence of a refinement mapping. A program is represented by a state machine (which may be infinite-state) specifying safety requirements (behaviour satisfies the property if it can be generated by a program); fairness constraints are represented by an arbitrary supplementary condition. A refinement mapping from a specification \(S_ 1\) to a specification \(S_ 2\) is a mapping from state space of \(S_ 1\) to state space of \(S_ 2\) which preserves state machine behaviour and liveness. Three cases when a refinement mapping does not exist are mentioned and it is shown how to overcome these problems by adding auxiliary variables (i.e. by adding internal state components not affecting the visible behaviour) to \(S_ 1\). The main result is a completeness theorem which states that, under three hypotheses about the specifications, if \(S_ 1\) implements \(S_ 2\) then one can add auxiliary, history and prophecy variables to \(S_ 1\) to form an equivalent \(S_ 1^{hp}\) and find a refinement mapping from \(S_ 1^{hp}\) to \(S_ 2\). Some examples demonstrate why these three hypotheses are needed.