State-Based Model Checking of Event-Driven System Requirements Export

@article{citeulike:3329085, abstract = {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.}, address = {Los Alamitos, CA, USA}, author = {Atlee, J. M. and Gannon, J.}, citeulike-article-id = {3329085}, citeulike-linkout-0 = {http://doi.ieeecomputersociety.org/10.1109/32.210305}, citeulike-linkout-1 = {http://dx.doi.org/10.1109/32.210305}, doi = {10.1109/32.210305}, issn = {0098-5589}, journal = {IEEE Transactions on Software Engineering}, keywords = {1993, event, modelchecking}, number = {1}, pages = {24--40}, posted-at = {2008-09-24 12:29:58}, priority = {2}, publisher = {IEEE Computer Society}, title = {State-Based Model Checking of Event-Driven System Requirements}, url = {http://dx.doi.org/10.1109/32.210305}, volume = {19}, year = {1993} }

TY - JOUR ID - citeulike:3329085 L3 - citeulike-article-id:3329085 N2 - 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. IS - 1 JF - IEEE Transactions on Software Engineering SN - 0098-5589 AD - Los Alamitos, CA, USA EP - 40 TI - State-Based Model Checking of Event-Driven System Requirements PB - IEEE Computer Society VL - 19 SP - 24 KW - 1993 KW - event KW - modelchecking AU - Atlee, JM AU - Gannon, J PY - 1993/// UR - http://dx.doi.org/10.1109/32.210305 ER -