The Community for Technology Leaders
Green Image
ABSTRACT
<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>
INDEX TERMS
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
CITATION
J. Gannon, J.M. Atlee, "State-Based Model Checking of Event-Driven System Requirements", IEEE Transactions on Software Engineering, vol. 19, no. , pp. 24-40, January 1993, doi:10.1109/32.210305
90 ms
(Ver 3.1 (10032016))