Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Third Annual IEEE Symposium on

Logic in Computer Science (LICS 1988)

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

Winner of the Test-of-Time Award in 2008
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 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

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}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski