Second IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'96)
Deriving Mode Invariants from SCR Specifications
Montreal, CANADA
October 21-October 25
ISBN: 0-8186-7614-0
This paper introduces a formal analysis method to derive modeclass invariants from Software Cost Reduction (SCR) specifications. SCR specifications can be used to specify event-driven systems. Mode invariants in SCR specifications are used to capture safety features that must be ensured during software development. This new method derives mode invariants from well-defined, consistent SCR specifications by transforming an SCR mode transition table into one matrix and two vectors to describe the conditions before and after a mode transition occurs, an algorithm then derives single mode invariants. A case study of a cruise control system shows that the algorithm is capable of determining the same mode invariants that were proved via model checking in earlier investigations.