Model Checking Complete Requirements Specifications Using Abstraction
Abstract
Although model checking has proven remarkably effective in detecting errors in hardware designs, its success in the analysis of software specifications has been quite limited. Model checking algorithms for hardware verification commonly use Binary Decision Diagrams (BDDs), a highly effective technique for analyzing specifications with the scores of Boolean variables commonly found in hardware descriptions. Unfortunately, BDDs are relatively ineffective for analyzing software specifications, which usually contain not only Booleans but variables spanning a wide range of data types. Further, software specifications have huge, often infinite, state spaces that cannot be model checked directly using conventional symbolic methods. One promising, but largely unexplored technique for limiting the size of the state space to be analyzed by model checking is to extract a model with a smaller state space from a complete specification using sound abstraction methods. Users of model checkers routinely analyze reduced models but most often generate the models in ad hoc ways. As a result, the reduced models are often incorrect. This paper first describes how one can model check a complete requirements specification expressed in the SCR (Software Cost Reduction) tabular notation. Unlike previous approaches which applied model checking to mode transition tables with Boolean variables, we use model checking to analyze properties of a complete SCR specification with variables ranging over many data types. The paper also describes two sound and complete methods for producing abstractions from requirements specifications. These abstractions are derived from the specification based on the property to be analyzed.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 10, 1997
- Accession Number
- ADA331870
Entities
People
- Constance Heitmeyer
- Ramesh Rharadwaj
Organizations
- United States Naval Research Laboratory