Verifying SCR Requirements Specifications Using State Exploration

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