When is `partial' adequate? A logic-based proof technique using partial specifications

TitleWhen is `partial' adequate? A logic-based proof technique using partial specifications
Publication TypeConference Papers
Year of Publication1990
AuthorsCleaveland R, Steffen B
Conference NameLogic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
Date Published1990/06/04/7
ISBN Number0-8186-2073-0
KeywordsCalculus, Carbon capture and storage, compositional proof rules, Computer science, Concurrent computing, Context, correctness, formal specification, logic-based proof technique, modal formula, parallel processes, partial process specification, partial specifications, specification adequacy, State-space methods, Technological innovation

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