Deriving mode invariants from SCR specifications
- 24 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
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, a comparison 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.Keywords
This publication has 5 references indexed in Scilit:
- Consistency Checks for SCR-Style Requirements SpecificationsPublished by Defense Technical Information Center (DTIC) ,1993
- State-based model checking of event-driven system requirementsIEEE Transactions on Software Engineering, 1993
- The Core method for real-time requirementsIEEE Software, 1992
- Software safety: why, what, and howACM Computing Surveys, 1986
- Specifying Software Requirements for Complex Systems: New Techniques and Their ApplicationIEEE Transactions on Software Engineering, 1980