The existence of refinement mappings.

*(English)*Zbl 0728.68083A 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.

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.

Reviewer: M.Křetínský (Brno)

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

PDF
BibTeX
Cite

\textit{M. Abadi} and \textit{L. Lamport}, Theor. Comput. Sci. 82, No. 2, 253--284 (1991; Zbl 0728.68083)

Full Text:
DOI

##### References:

[1] | Alpera, B.; Schneider, F.B., Recognizing safety and liveness, () · Zbl 0641.68039 |

[2] | Alpern, B.; Schneider, F.B., Proving Boolean combinations of deterministic properties, (), 131-137 |

[3] | Herlihy, M.P.; Wing, J.M., Axioms for concurrent objects, (), 13-26, Munich |

[4] | Jonsson, B., Compositional verification of distributed systems, () |

[5] | Knuth, D.E., Fundamental algorithms. the art of computer programming, vol. 1, (1973), Addison-Wesley Reading, MA · Zbl 0191.17903 |

[6] | Lamport, L., Proving the correctness of multiprocess programs, IEEE trans. software engineering, 3, 2, 125-143, (1977) · Zbl 0349.68006 |

[7] | Lamport, L., Specifying concurrent program modules, ACM trans. programming languages and systems, 5, 2, 190-222, (1983) · Zbl 0516.68010 |

[8] | Lam, S.S.; Shankar, A.Udaya, Protocol verification via projections, IEEE trans. software engineering, 10, 4, 325-342, (1984) · Zbl 0552.68022 |

[9] | Lynch, N.; Tuttle, M., Hierarchical correctness proofs for distributed algorithms, (), 137-151 |

[10] | Merritt, M., Completeness theorems for automata, (), 544-560 |

[11] | Manna, Z.; Pnueli, A., Specification and verification of concurrent programs by ∀-automata, (), 1-12 |

[12] | Owicki, S., Axiomatic proof techniques for parallel programs, () · Zbl 0395.68015 |

[13] | Stark, E.W., Proving entailment between conceptual state specifications, Theoret. comput. sci., 56, 1, 135-154, (1988) · Zbl 0632.68026 |

[14] | Vardi, M., Verification of concurrent programs: the automata-theoretic framework, (), 167-176 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.