×

Refinement and composition of transition-based rely-guarantee specifications with auxiliary variables. (English) Zbl 0733.68054

Foundations of software technology and theoretical computer science, Proc. 10th Conf., Bangalore/India 1990, Lect. Notes Comput. Sci. 472, 332-348 (1990).
Summary: [For the entire collection see Zbl 0731.00025.]
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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

Citations:

Zbl 0731.00025