Refinement and composition of transition-based rely-guarantee specifications with auxiliary variables

Abstract

We combine two ideas for specification and verification of concurrent systems: The rely-guarantee paradigm and transition-based specification. We consider specification of safety properties of shared variable systems. A component is specified by stating which transitions its environment is allowed to make to the interface variables and which changes the component then guarantees to stay within. Auxiliary variables are used to carry history information. For such specifications, we present proof rules for verifying that one specification refines another and that parallel composition of components implements a given specification. Application of the rules is illustrated by small examples.