Paper: The existence of refinement mappings (at LICS 1988)

Authors: Martín Abadi Leslie Lamport

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

BibTeX

  @InProceedings{AbadiLamport-Theexistenceofrefin,
    author = 	 {Martín Abadi and Leslie Lamport},
    title = 	 {The existence of refinement mappings},
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {165--175},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }