Writing requirements in a formal notation permits automatic assessment of such properties as ambiguity, consistency, and completeness. However, verifying that the properties expressed in requirements are preserved in other software life cycle artifacts remains difficult.
This dissertation describes methods and tools for automatically analyzing the consistency of software requirements and detailed designs. Requirements describe systems as state machines with event-driven transitions using a specification language that is easy to read and scalable to large systems. We have defined consistency between requirements and detailed designs to be that exactly the same transitions and global safety properties specified in the requirements are preserved in the designs. To judge global properties like these, we determine the possible system states which exist at different points in designs. The detailed bookkeeping necessary to do this exceeds the capabilities of human reviewers for all but small systems.
We have developed a language for specifying detailed designs, an analysis technique to create a model of a design through abstract interpretation of the language constructs, and a method to automatically generate and check properties derived from requirements to ensure a design's consistency with them. These ideas are implemented in a tool which is capable of analyzing designs with multiple procedures and processes. Using our tool, we were able to uncover errors in designs of existing sequential systems and analyze our own designs of concurrent systems.