A logic-model semantics for SCR software requirements

ABSTRACT

This paper presents a simple logic-model semantics for Software Cost Reduction (SCR) software requirements. Such a semantics enables model-checking of native SCR requirements and obviates the need to transform the requirements for analysis. The paper also proposes modal-logic abbreviations for expressing conditioned events in temporal-logic formulae. The Symbolic Model Verifier (SMV) is used to verify that an SCR requirements specification enforces desired global requirements, expressed as formulae in the enhanced logic. The properties of a small system (an automobile cruise control system) are verified, including an invariant property that could not be verified previously. The paper concludes with a discussion of how other requirements notations for conditioned-event-driven systems could be similarly checked.

REFERENCES

• 1: T. Alspaugh, S. Faulk, K. Britton, R. Parker, D. Parnas, and J. Shore. Software Requirements for the A-7E Aircraft. Technical report, Naval Research Laboratory, March 1988.
• 2: Joanne Marie Atlee, Automated analysis of software requirements, University of Maryland at College Park, College Park, MD, 1992
• 3: J. M. Atlee , J. Gannon, State-Based Model Checking of Event-Driven System Requirements, IEEE Transactions on Software Engineering, v.19 n.1, p.24-40, January 1993 [doi>10.1109/32.210305]
• 4: M. C Browne, Automatic verification of finite state machines using temporal logic, Carnegie Mellon University, Pittsburgh, PA, 1989
• 5: J. Butch, E. Clarke, K. McMillan, D. Dill, and j. Hwang. "Symbolic Model Checking: 102o S~a~es and Beyond". In Proceedings of the 5th Annual Symposium on Logic in Computer Science, pages 428-439, June 1990.
• 6: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 7: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 8: C. Heitmeyer. "Tools for Analyzing Requirements: A Formal Foundation", December 1994. Presented at the Fourth International SCR Workshop.
• 9: C. Heitmeyer. Private communications, September 1995.
• 10: C. Heitmeyer , B. Labaw , D. Kiskis, Consistency checking of SCR-style requirements specifications, Proceedings of the Second IEEE International Symposium on Requirements Engineering, p.56, March 27-29, 1995
• 11: K. Heninger. "Specifying Software Requirements for Complex Systems: New Techniques and Their Applications". IEEE Transactions on Software Engineering, SE-6(1):2-12, January 1980.
• 12: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 13: J. Kirby. Example NRL/SCR Software Requirements for an Automobile Cruise Control and Monitoring System. Technical Report TR-87-07, Wang Institute of Graduate Studies, July 1987.
• 14: Nancy G. Leveson , Mats Per Erik Heimdahl , Holly Hildreth , Jon D. Reese, Requirements Specification for Process-Control Systems, IEEE Transactions on Software Engineering, v.20 n.9, p.684-707, September 1994 [doi>10.1109/32.317428]
• 15: Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem, Carnegie Mellon University, Pittsburgh, PA, 1992
• 16: D. Parnas and J. Madey. Functional Documentation for Computer Systems Engineering (Version 2). Technical Report CRL Report 237, Department of Electrical and Computer Engineering, Mc- Master University, 1991.
• 17: J. van Schouwen. The A-7 Requirements Model: Re-examination for Real-Time Systems and an Application to Monitoring Systems. Technical Report TP~-90-276, Department of Computing and Information Science, Queen's University, Kingston, On{ario, May 1990.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Model theory

General Terms:
Design, Theory, Verification

Keywords:
formal semantics, model checking, reactive systems, software requirements