Issue No. 01 - January (1993 vol. 19)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.210305
<p>It is demonstrated how model checking can be used to verify safety properties for event-driven systems. SCR tabular requirements describe required system behavior in a format that is intuitive, easy to read, and scalable to large systems (e.g. the software requirements for the A-7 military aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. An automated technique for formalizing the semiformal SCR requirements and for transforming the resultant formal specification onto a finite structure that a model checker can analyze has been developed. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system.</p>
event-driven system requirements; model checking; SCR tabular requirements; software requirements; A-7 military aircraft; temporal logics; formal specification; system invariants; automobile cruise control system; water-level monitoring system; formal specification; formal verification
J. Gannon and J. Atlee, "State-Based Model Checking of Event-Driven System Requirements," in IEEE Transactions on Software Engineering, vol. 19, no. , pp. 24-40, 1993.