The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.01 - January (1993 vol.19)
pp: 24-40
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.M. Atlee, "State-Based Model Checking of Event-Driven System Requirements", IEEE Transactions on Software Engineering, vol.19, no. 1, pp. 24-40, January 1993, doi:10.1109/32.210305
102 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool