Back to Search
Start Over
State-Based Model Checking of Event-Driven System Requirements.
- Source :
-
IEEE Transactions on Software Engineering . Jan93, Vol. 19 Issue 1, p24-40. 17p. 9 Diagrams, 6 Charts. - Publication Year :
- 1993
-
Abstract
- In this paper, we demonstrate 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 A7 aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. We have developed 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. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 00985589
- Volume :
- 19
- Issue :
- 1
- Database :
- Academic Search Index
- Journal :
- IEEE Transactions on Software Engineering
- Publication Type :
- Academic Journal
- Accession number :
- 14306085
- Full Text :
- https://doi.org/10.1109/32.210305