Lazy Compositional Verification

Abstract

Classical methods for the verification of concurrent systems are effective for reasoning about global properties of small systems. For larger systems, these approaches become expensive both in terms of computational and human effort. A compositional verification methodology can reduce the verification effort by allowing global system properties to be derived from local component properties. Most compositional verification methods are based on the assume-guarantee paradigm where component properties are verified contingent on properties that are assumed of the environment. Component properties are composed by showing that the properties guaranteed by a component entail the assumptions of the others. We describe an alternate paradigm called lazy composition where component properties are proved by composing the component description with an abstract environment. The demonstration that each component uses a correct abstraction of its environment is carried out lazily as the design details emerge. We present the main ideas underlying lazy composition along with illustrative examples, and contrast it with the assume-guarantee approach.

Relevant Papers

Transparencies