A logic-model semantics for SCR software requirements

Abstract

This paper presents a simple logic-model semantics for Software Cost Reduction (SCR) software requirements. Such a semantics enables model-checking of native SCR requirements and obviates the need to transform the requirements for analysis. The paper also proposes modal-logic abbreviations for expressing conditioned events in temporal-logic formulae. The Symbolic Model Verifier (SMV) is used to verify that an SCR requirements specification enforces desired global requirements, expressed as formulae in the enhanced logic. The properties of a small system (an automobile cruise control system) are verified, including an invariant property that could not be verified previously. The paper concludes with a discussion of how other requirements notations for conditioned-event-driven systems could be similarly checked.