Automatic analysis of consistency between requirements and designs

Writing requirements in a formal notation permits automatic assessment of s uch properties as ambiguity. consistency, and completeness. However, verify ing that the properties expressed in requirements are preserved in other so ftware life cycle artifacts remains difficult. The existing techniques eith er require substantial manual effort and skill or suffer from exponential e xplosion of the number of states in the generated state spaces. "Light-weig ht" formal methods is an approach to achieve scalability in fully automatic verification by checking an abstraction of the system for only certain pro perties. This paper describes light-weight techniques for automatic analysi s of consistency between software requirements (expressed in SC R) and deta iled designs in low-deg ree-polynomial time, achieved at the expense of usi ng imprecise data-flow analysis techniques. A specification language SCR de scribes the systems as state machines with event-driven transitions. We def ine detailed designs to be consistent with their SCR requirements if they c ontain exactly the same transitions. We have developed a language for speci fying detailed designs, an analysis technique to create a model of a design through data-flow analysis of the language constructs, and a method to aut omatically generate and check properties derived from requirements to ensur e a design's consistency with them. These ideas are implemented in a tool n amed CORD, which we used to uncover errors in designs of some existing syst ems.