Existing methodologies for the verification of concurrent systems are effective for reasoning about global properties of small systems. For large 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. For this to work, each component must be viewed as an open system interacting with a well-behaved environment. Much of the emphasis in compositional verification has been on the assume-guarantee paradigm where component properties are verified contingent on properties that are assumed of the environment. We highlight an alternate paradigm called lazy composition where the component properties are proved by composing the component with an abstract environment. We present the main ideas underlying lazy composition along with illustrative examples, and contrast it with the assume-guarantee approach. The main advantage of lazy composition is that the proof that one component meets the expectations of the other components, can be delayed till sufficient detail has been added to the design.
CITATION STYLE
Shankar, N. (1998). Lazy compositional verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1536, pp. 541–564). Springer Verlag. https://doi.org/10.1007/3-540-49213-5_21
Mendeley helps you to discover research relevant for your work.