TitleVerifying SCR Requirements Specifications using State Exploration
Publication TypeConference Paper
Year of Publication1997
AuthorsBharadwaj, R., and C. L. Heitmeyer
Conference NameFirst ACM SIGPLAN Workshop on Automatic Analysis of Software
Conference LocationParis, France
Abstract

Researchers at the Naval Research Laboratory (NRL) have been developing a formal method, known as the SCR (Software Cost Reduction) method, to specify the requirements of software systems using tables. NRL has developed a formal state machine model defining the SCR semantics and support tools for analysis and validation. Recently, a verification capability was added to the SCR toolset. Users can now invoke the Spin model checker within the toolset to establish properties of a specification. This paper describes the results of our initial experiments to verify properties of SCR requirements specifications using Spin. After reviewing the SCR requirements method and introducing our formal requirements model, we describe how SCR specifications can be translated into an imperative programming notation. We also describe how we limit state explosion by verifying abstractions of the original requirements specification. These abstractions are derived using the formula to be verified and special attributes of SCR specifications. The paper concludes with the results of our experiments with Spin and a discussion of ongoing and future work.

Full Text

BharadwajHeitmeyer1997.pdf

NRL Publication Release Number

07-1221.1-0385