Lics

IEEE Symposium on Logic in Computer Science

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

Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

Paper: When is `partial' adequate? A logic-based proof technique using partial specifications (at LICS 1990)

Authors: Rance Cleaveland Bernhard Steffen

Abstract

A technique is presented for ascertaining when a (finite-state) partial process specification is adequate, in the sense of being specified enough, for contexts in which it is to be used. The method relies on the automatic generation of a modal formula from the partial specification; if the remainder of the network satisfies this formula, then any process that meets the specification is guaranteed to ensure correct behavior of the overall system. Using the results, the authors develop compositional proof rules for establishing the correctness of networks of parallel processes and illustrate their use with several examples

BibTeX

  @InProceedings{CleavelandSteffen-Whenispartialadequa,
    author = 	 {Rance Cleaveland and Bernhard Steffen},
    title = 	 {When is `partial' adequate? A logic-based proof technique using partial specifications },
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {440--449},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski