This Article 
 Bibliographic References 
 Add to: 
State-Based Model Checking of Event-Driven System Requirements
January 1993 (vol. 19 no. 1)
pp. 24-40

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.

[1] T. Alspaugh, S. Faulk, K. Britton, R. Parker, D. Parnas, and J. Shore, "Software requirements for the A-7E Aircraft," Naval Research Lab., Tech. Rep., March 1988.
[2] J. Atlee, "Automated analysis of software requirements," Ph.D. dissertation, Dept. of Computer Science, University of Maryland, College Park, MD, 1992.
[3] J. Atlee and J. Gannon, "State-based model checking of event-driven system requirements," inProc. ACM SIGSOFT'91 Conf. Software for Critical Systems, 1991, pp. 16-28.
[4] W. W. Bledsoe and L. Hines, "Variable elimination and chaining in a resolution-based prover for inequalities," inProc. 5th Conf. on Auto. Deduction, 1980, pp. 281-292.
[5] M. Browne, "Automatic verification of finite state machines using temporal logic," Ph.D. dissertation, Dept. of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 1989.
[6] M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra, "Automatic verification of sequential circuits using temporal logic,"IEEE Trans. Computers, vol. C-35, pp. 1035-1044, Dec. 1986.
[7] J. B. Burchet al., "Symbolic model checking: 1020states and beyond," inProc. 5th Symp. Logics in Computer Science, pp. 428-439, IEEE Computer Society Press, 1990.
[8] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.
[9] E. M. Clarke, D. E. Long, and K. L. McMillan, "A language for compositional specification and verification of finite state hardware controllers,"Proc. IEEE, vol. 79, pp. 1283-1292, Sept. 1991.
[10] M. Degl'Innocenti, G. Ferrari, G. Pacini, and F. Turini, "RSF: A formalism for executable requirements specifications,"IEEE Trans. Software Eng., vol. 16, no. 11, pp. 1235-1246, Nov. 1990.
[11] E. Emerson and E. Clarke, "Using branching time temporal logic to synthesize synchronization skeletons,"Sci. Comput. Programming, vol. 2, pp. 241-266, 1982.
[12] S. Faulk, "State determination in hard-embedded systems," Ph.D. dissertation, Dept. of Computer Science, University of North Carolina, Chapel Hill, 1989.
[13] A. Gabrielian and M. Franklin,"Multilevel specification of real-time systems,"Comm. of ACM 34, pp. 51-60, May 1991.
[14] A. Gabrielian and R. Iyer, "Integrating automata and temporal logic: A framework for specification of real-time systems and software," inProc. Unified Computation Laboratory, 1990.
[15] C. Ghezzi, D. Mandrioli, and A. Morzenti, "TRIO: A logic language for executable specifications of real-time systems,"J. Systems Software, vol. 12, pp. 107-123, 1990.
[16] D. Harel, "Statecharts: A visual formalism for complex systems,"Sci. Comput. Program., vol. 8, pp. 231-274, 1987.
[17] D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot, "STATEMATE: A working environment for the development of complex reactive systems,"IEEE Trans. Software Eng., vol. 16, no. 4, pp. 403-414, April 1990.
[18] C. Heitmeyer and B. Labaw, "Consistency checks for SCR-style requirements specifications," in preparation.
[19] K. Heninger, "Specifying software requirements for complex systems: New techniques and their applications,"IEEE Trans. Software Eng., vol. SE-6, no. 1, pp. 2-12, Jan. 1980.
[20] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[21] J. Kirby, "Example NRL/SCR software requirements for an automobile cruise control and monitoring system," Wang Institute of Graduate Studies, Tech. Rep. TR-87-07, July 1987.
[22] Z. Manna and A. Pnueli, "Tools and Rules for the Practicing Verifier," Tech. Report Stan-CS-90-1321, Computer Science Dept., Stanford University, Stanford, Calif., 1990.
[23] J. Ostroff,Temporal Logic of Real-Time Systems. Research Studies Press, 1990.
[24] D. Parnas, D. Smith, and T. Pearce, "Making formal software documentation more practical: A progress report," Dept. of Computing and Information Science, Queen's University, Kingston, Ontario, Canada, Tech. Rep. TR-88-236, 1988.
[25] A. Pnueli, "The temporal logic of programs," inProc. 18th Annu. Symp. the Foundation of Computer Science, 1977, pp. 46-57.
[26] S. Smith and S. Gerhart, "STATEMATE and cruise control: A case2study," inProc. COMPAC'88, 12th Int. IEEE Computer Software and Application Conf., 1988, pp. 49-56.
[27] J. van Schouwen, "The A-7 requirements model: Reexamination for real-time systems and an application to monitoring systems," Dept. of Computing and Information Science, Queens's University, Kingston, Ontario, Canada, Tech. Rep. TR-90-276, May 1990.
[28] J. van Schouwen, private communication, 1991.
[29] D. Weiss, private communication, 1992.

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
J.M. Atlee, J. Gannon, "State-Based Model Checking of Event-Driven System Requirements," IEEE Transactions on Software Engineering, vol. 19, no. 1, pp. 24-40, Jan. 1993, doi:10.1109/32.210305
Usage of this product signifies your acceptance of the Terms of Use.