Automated integrative analysis of state-based requirements

Statically analyzing requirements specifications to assure that they possess desirable properties is an important activity in any rigorous software development project. The analysis is performed on an abstraction of the original requirements specification. Abstractions in the model may lead to spurious errors in the analysis output. Spurious errors are conditions that are reported as errors, but information abstracted out of the model precludes the reported conditions from being satisfied. A high ratio of spurious errors to true errors in the analysis output makes it difficult, error-prone, and time consuming to find and correct the true errors. We describe an iterative and integrative approach for analyzing state-based requirements that capitalizes on the strengths of a symbolic analysis component and a reasoning component while circumventing their weaknesses. The resulting analysis method is fast enough and automated enough to be used on a day-to-day basis by practicing engineers, and generates analysis reports with a small ratio of spurious errors to true errors