The verification of concurrent systems with a large number of interacting components poses a significant challenge to existing verification methodologies. We present a simple approach to compositional verification that allows global system properties to be established by considering only the behavior of the relevant system components. Each component specification describes the transitions due to the component itself and constrains the transitions due its environment. The composition of two specifications is an interleaving conjunction of the two specifications. Every property derived from a component specification remains true when this component is composed with other components. This compositional approach to verification is illustrated with the example of a buffer composed from two smaller buffers, and a real-time controller for a railroad crossing system composed from the subsystems for trains, the controller, and the gate. These examples have been verified using the PVS verification system.

• csl-93-8.dvi
• csl-93-8.ps