Third Annual IEEE Symposium on

Logic in Computer Science (LICS 1988)

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

Authors: Martín Abadi Leslie Lamport


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


    author = 	 {Martín Abadi and Leslie Lamport},
    title = 	 {The existence of refinement mappings},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {165--175},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}