Automatic generation of state invariants from requirements specifications

ABSTRACT

Automatic generation of state invariants, properties that hold in every reachable state of a state machine model, can be valuable in software development. Not only can such invariants be presented to system users for validation, in addition, they can be used as auxiliary assertions in proving other invariants. This paper describes an algorithm for the automatic generation of state invariants that, in contrast to most other such algorithms, which operate on programs, derives invariants from requirements specifications. Generating invariants from requirements specifications rather than programs has two advantages: 1) because requirements specifications, unlike programs, are at a high level of abstraction, generation of and analysis using such invariants is easier, and 2) using invariants to detect errors during the requirements phase is considerably more cost-effective than using invariants later in software development. To illustrate the algorithm, we use it to generate state invariants from requirements specifications of an automobile cruise control system and a simple control system for a nuclear plant. The invariants are derived from specifications expressed in the SCR (Software Cost Reduction) tabular notation.

REFERENCES

• 1: ALSPAUGH, T. A., FAULK, S. R., BRITTON, K. H., PARKER, R. A., PARNAS, D. L., AND SHORE, J. E. Software requirements for the A- 7E aircraft. Tech. Rep. NRL-9194, Naval Research Lab., Wash., DC, 1992.
• 2: ARCHER, M., AND HEITMEYER, C. The use of model checking and abstraction in analyzing requirements specifications: A formal foundation. Tech. rep., Naval Research Lab., Washington, DC, 1998. (Draft).
• 3: Joanne Marie Atlee, Automated analysis of software requirements, University of Maryland at College Park, College Park, MD, 1992
• 4: 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]
• 5: Saddek Bensalem , Yassine Lakhnech , Hassen Saïdi, Powerful Techniques for the Automatic Generation of Invariants, Proceedings of the 8th International Conference on Computer Aided Verification, p.323-335, August 03, 1996
• 6: Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999 [doi>10.1023/A:1008697817793]
• 7: Nikolaj Bjørner , Anca Browne , Zohar Manna, Automatic generation of invariants and intermediate assertions, Theoretical Computer Science, v.173 n.1, p.49-87, Feb. 1997 [doi>10.1016/S0304-3975(96)00191-0]
• 8: M. C Browne, Automatic verification of finite state machines using temporal logic, Carnegie Mellon University, Pittsburgh, PA, 1989
• 9: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 10: CROW, J., OWRE, S., RUSHBY, J., SHANKAR, N., AND SRIVAS, M. A tutorial introduction to PVS. Tech. rep., Computer Science Lab, SRI Int'l, Menlo Park, CA, Apr. 1995. (Presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL).
• 11: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 12: FAULIC, S. R., FINNERAN, L., KIRBY, JR., J., SHAH, S., AND SUTTON, J. Esperience applying the CORE method to the Lockheed C-130J. In Proc. gfh Annual Conf. on Computer Assurance (COdlPASS ' $4) (Gaithersburg, MD, June 1994), pp. 3-8.
• 13: Susanne Graf , Hassen Saïdi, Verifying Invariants Using theorem Proving, Proceedings of the 8th International Conference on Computer Aided Verification, p.196-207, August 03, 1996
• 14: David Harel , Amnon Naamad, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.293-333, Oct. 1996 [doi>10.1145/235321.235322]
• 15: Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998 [doi>10.1109/32.730543]
• 16: Constance L. Heitmeyer , James Kirby , Bruce G. Labaw , Ramesh Bharadwaj, SCR*: A Toolset for Specifying and Analyzing Software Requirements, Proceedings of the 10th International Conference on Computer Aided Verification, p.526-531, June 28-July 02, 1998
• 17: Constance L. Heitmeyer , Ralph D. Jeffords , Bruce G. Labaw, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.231-261, July 1996 [doi>10.1145/234426.234431]
• 18: HEIThIEYER, C. L., KIRBY, JR., J., AND LABAW, B. G. Tools for formal specification, verification, and validation of requirements. In PTOC. 12fh Annual Conf. on Computer Assurance (COM- PASS' 97) (Gaithersburg, MD, June 1997), IEEE.
• 19: HENINGER, K., PARNAS, D. L., SHORE, J. E., AND KALLANDER, J. W. Software requirements for t'he A-7E aircraft. Tech. Rep. 3876, Naval Research Lab., Wash., DC, 1978.
• 20: HENINGER, K. L. Specifying software requiremen& for complex systems: Nelv techniques and their application. IEEE Trans. Soffw. Eng. SE-6, 1 (Jan. 1980), 2-13.
• 21: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 22: JEFFORDS, R. D., AND HEITIEYER, C. L. Efficient automatic generation of state invariants from esecut,able requirements specifications. Tech. rep., Naval Research Lab., Washington DC, 1998. (Draft).
• 23: KIRBY, JR., J. Example NRL/SCR softlvare requirements for an automobile cruise control and monitoring system. Tech. Rep. TR-87-07, Wang Inst. of Graduate Studies, Tyngsboro, MA, July 1987.
• 24: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 25: 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]
• 26: C. Loiseaux , S. Graf , J. Sifakis , A. Bouajjani , S. Bensalem, Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, v.6 n.1, p.11-44, Jan. 1995 [doi>10.1007/BF01384313]
• 27: Z Manna , Anuchit Anuchitanukul , Nikolaj Bjorner , Anca Browne , Edward Chang , Michael Colon , Luca de Alfaro , Harish Devarajan , Henny Sipma , Tomas Uribe, STeP: The Stanford Temporal Prover, Stanford University, Stanford, CA, 1994
• 28: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 29: Jonathan S. Ostroff, Temporal logic for real time systems, John Wiley & Sons, Inc., New York, NY, 1989
• 30: OWRE, S., SHANKAR, N., AND RUSHBY, J. User guide for the PVS specification and verification system (Draft). Tech. rep., Computer Science Lab, SRI Int'l, Menlo Park, CA, 1993.
• 31: David Y. W. Park , Jens U. Skakkebæk , David L. Dill, Static Analysis to Identify Invariants in RSML Specifications, Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.133-142, September 14-18, 1998
• 32: David Lorge Parnas , Jan Madey, Functional documents for computer systems, Science of Computer Programming, v.25 n.1, p.41-61, Oct. 1995 [doi>10.1016/0167-6423(95)96871-J]
• 33: SREEMANI, T., AND ATLEE, J. M. Feasibility of model checking software requirements: A case study. In PTOC. 11th Annual Conference on Computer Assurance (COhfPASS ' 96) (Gaithersburg, MD, June 1996), pp. 77-88.
• 34: Jeffrey X. Su , David L. Dill , Clark W. Barrett, Automatic Generation of Invariants in Processor Verification, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.377-388, November 06-08, 1996

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.3 Software Management
          Subjects: Software development

General Terms:
Algorithms, Design, Measurement, Performance, Theory, Verification

Keywords:
formal methods, invariants, requirements, software tools, specification, validation, verification