Verification of consistency between concurrent program designs and their requirements

Writing requirements in a formal notation allows the automatic assessment of such properties as ambiguity, consistency and completeness. However, verifying that the properties expressed in the requirements are preserved in an implementation remains difficult. In our earlier work (1995), we described a technique for analyzing the consistency of detailed program designs with their requirements. To ensure that our methods scale up to realistic systems, we need to develop compositional approaches. This paper describes a first step in this direction: a technique for analyzing concurrent program designs. We present a language for specifying detailed designs of concurrent programs and an analysis tool, called Analyzer, which uses this language to build a finite-state abstraction of the design. This abstraction is compared with properties derived from the set of requirements to determine if the former is consistent with the latter. Some restrictions on the model and on the specification language enable Analyzer to verify global user-specified properties effectively. After a design has been verified to be consistent with its requirements, an implementation can be written around the design constructs to reduce the likelihood of implementation errors