DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
ADA331870
Title:
Model Checking Complete Requirements Specifications Using Abstraction
Descriptive Note:
Memo. rept.
Corporate Author:
NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR COMPUTER HIGH ASSURANCE SYSTEMS
Report Date:
1997-11-10
Pagination or Media Count:
32.0
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.
Distribution Statement:
APPROVED FOR PUBLIC RELEASE
