Verifying SCR Requirements Specifications Using State Exploration

How SCR specifications can be translated into an imperative programming notation is described and how to limit state explosion by verifying abstractions of the original requirements specification is described.

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.