Automatic verification of requirements implementation

ABSTRACT

Requirements of event-based systems can be automatically analyzed to determine if certain safety properties hold. However, we lack comparable methods to verify that implementations maintain the properties guaranteed by the requirements. We have built a tool that compares implementations written in C with their requirements. Requirements describe events which cause state transitions. Implementations are annotated to describe changes in the values of their requirement's variables, and dataflow analysis techniques are used to determine the set of events which cause particular state changes. To show that an implementation is consistent with its requirements, we show that each event causing a change of state in the implementation appears in the requirements, and that all the events specified to cause state changes in the requirements appear in the implementation. The annotation language encourages programmers to describe local program behaviors. These behaviors are collected into system-level behaviors, which are compared to those in the requirements. Since our analysis is not based on program code, annotations can describe behaviors at any level of granularity. We illustrate the use of our tool with several different annotations of a temperature-control system.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: 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.
• 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: Patrick Cousot and Radhia Cousot. "Static Determination of Dynamic Properties of Programs". In Proceedings of the "Colloque sue la Prograrnmation', April 1976.
• 5: C. Heitmeyer and B. Labaw. "Consistency Checks for SCR-Style Requirements Specifications". Technical Report NRL Report 93-9586, Naval Research Laboratory, November 1993.
• 6: K. Heninger. "Specifying Software Requirements for Complex Systems: New Techniques and Their Applications". IEEE Transactions on Software En. gineering, SE-6(1):2-12, January 1980.
• 7: William E. Howden, Comments Analysis and Programming Errors, IEEE Transactions on Software Engineering, v.16 n.1, p.72-81, January 1990 [doi>10.1109/32.44365]
• 8: Daniel Jackson, Abstract analysis with aspect, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.19-27, June 28-30, 1993, Cambridge, Massachusetts, United States
• 9: B.H. Liskov and S.N. Zilles. "Specification Techniques for Data Abstraction". IEEE Transactions on Software Engineering, SE-1(1):7-18, March 1975.
• 10: K. Olender , L. Osterweil, Cesar: a static sequencing constraint analyzer, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.66-74, December 13-15, 1989, Key West, Florida, United States
• 11: Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990 [doi>10.1109/32.48935]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: C

General Terms:
Algorithms, Design, Languages, Verification