This Article 
 Bibliographic References 
 Add to: 
Automatic Analysis of Consistency between Requirements and Designs
July 2001 (vol. 27 no. 7)
pp. 651-672

Abstract—Writing requirements in a formal notation permits automatic assessment of such properties as ambiguity, consistency, and completeness. However, verifying that the properties expressed in requirements are preserved in other software life cycle artifacts remains difficult. The existing techniques either require substantial manual effort and skill or suffer from exponential explosion of the number of states in the generated state spaces. “Light-weight” formal methods is an approach to achieve scalability in fully automatic verification by checking an abstraction of the system for only certain properties. This paper describes light-weight techniques for automatic analysis of consistency between software requirements (expressed in SCR) and detailed designs in low-degree-polynomial time, achieved at the expense of using imprecise data-flow analysis techniques. A specification language SCR describes the systems as state machines with event-driven transitions. We define detailed designs to be consistent with their SCR requirements if they contain exactly the same transitions. We have developed a language for specifying detailed designs, an analysis technique to create a model of a design through data-flow analysis of the language constructs, and a method to automatically generate and check properties derived from requirements to ensure a design's consistency with them. These ideas are implemented in a tool named cord, which we used to uncover errors in designs of some existing systems.

[1] A.V. Aho, R. Sethi, and J.D. Ullman, Compilers, Principles, Techniques and Tools.New York: Addison-Wesley, 1985.
[2] T. Alspaugh, S. Faulk, K. Britton, R. Parker, D. Parnas, and J. Shore, “Software Requirements for the A-7E Aircraft,” technical report, US Naval Research Lab., Mar. 1988.
[3] S. Anderson and G. Bruns, “The Formalization and Analysis of a Communications Protocols,” Formal Aspects of Computing, vol. 6, pp. 92–112, 1994.
[4] G. Archinoff, R. Hohendorf, A. Wassyng, B. Quigley, and M. Borsch, “Verification of the Shutdown System Software at the Darlington Nuclear Generation Station,” Proc. Int'l Conf. Control and Instrumentation in Nuclear Installations, May 1990.
[5] J. Atlee, “Automated Analysis of Software Requirements,” PhD thesis, Univ. of Maryland, College Park, MD, Dec. 1992.
[6] J.M. Atlee and J. Gannon, "State-Based Model Checking of Event-Driven System Requirements," IEEE Trans. Software Eng., vol. 19, no. 1, pp. 24-40, Jan. 1993.
[7] R. Bharadwaj and C. Heitmeyer, "Model Checking Complete Requirements Specifications Using Abstraction," Automated Software Eng. J., vol. 6, no. 1, Jan. 1999.
[8] F.P. BrooksJr., "No Silver Bullet—Essence and Accidents of Software Engineering," Computer, vol. 20, no. 4, Apr. 1987, pp. 10-19.
[9] S.H. Caine and E.K. Gordon, “PDL: A Tool for Software Design,” Proc. Nat'l Computer Conf., vol. 44, pp. 271–276, 1975.
[10] M. Chechik, Automatic Analysis of Consistency between Requirements and Designs, PhD thesis, Univ. of Maryland, College Park, MD, Dec. 1996.
[11] M. Chechik, “$\rm SC(R)^3$: Towards Usability of Formal Methods,” Proc. CASCON'98, pp. 177–191, Nov. 1998.
[12] M. Chechik and J. Gannon, “Automatic Verification of Requirements Implementations,” Proc. 1994 Int'l Symp. Software Testing and Analysis (ISSTA), pp. 1–14, Aug. 1994.
[13] M. Chechik and J. Gannon, “Automatic Analysis of Consistency Between Implementations and Requirements: A Case Study,” Proc. 10th Ann. Conf. Computer Assurance, pp. 123–131, June 1995.
[14] M. Chechik and V.S. Sudha, “Checking Consistency between Source Code and Annotations,” CSRG Technical Report 373, Dept. of Computer Science, Univ. of Toronto, 1998.
[15] G. Chehaibar, H. Garavel, L. Mounier, N. Tawbi, and F. Zulian, “Specification and Verification of the Powerscale Bus Arbitration Protocol: An Industrial Experiment with LOTOS,” Proc. Joint Int'l Conf. Formal Description Techniques for Distributed Systems and Comm. Protocols, and Protocol Specification, Testing, and Verification FORTE/PSTV '96, 1996.
[16] E. Clarke, S. German, and X. Zhao, “Verifying the SRT Division Algorithm Using Theorem Proving Techniques,” Proc. Eighth Int'l Conf. Computer-Aided Verification, pp. 111–122, July 1996.
[17] E.M. Clarke, O. Grumberg, and D.E. Long, “Model Checking and Abstraction,” IEEE Trans. Programming Languages and Systems, vol. 19, no. 2, 1994.
[18] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[19] E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. Long, K.L. McMillan, and L.A. Ness, “Verification of the Futurebus+ Cache Coherence Protocol,” Formal Methods in System Design, vol. 6, pp. 217–232, 1995.
[20] R. Cleaveland, J. Parrow, and B. Steffen, "The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems," ACM Trans. Programming Languages and Systems, Jan. 1993, pp. 36-72.
[21] P.C. Clements, C.L. Heitmeyer, B.G. Labaw, and A.T. Rose, “MT: A Toolset for Specifying and Analyzing Real-Time Systems,” Proc. IEEE Real-Time Systems Symp., Dec. 1993.
[22] A.J. Dill, D.L. Drexler, A.J. Hu, and C.H. Yang, “Protocol Verification as a Hardware Design Aid,” Proc. IEEE Int'l Conf. Computer Design: VLSI in Computers and Processors, 1992.
[23] S. Easterbrook, R. Lutz, R. Covington, Y. Ampo, and D. Hamilton, "Experiences Using Lightweight Formal Methods for Requirements Modeling," IEEE Trans. Software Eng., vol. 24, no. 1, Jan. 1998.
[24] D. Evans, “Static Detection of Dynamic Memory Errors,” Proc. SIGPLAN '96 Conf. Programming Language Design and Implementation, pp. 44–53, May 1996.
[25] D. Evans, J. Guttag, J. Horning, and Y.M. Tan, “LCLint: A Tool for Using Specifications to Check Code,” Proc. Second ACM SIGSOFT Symp. the Foundations of Software Eng. (SIGSOFT '94), pp. 87–97, Dec. 1994.
[26] S. Faulk, “State Determination in Hard-Embedded Systems,” PhD thesis, Univ. of North Carolina, Chapel Hill, NC, 1989.
[27] O. Grumberg and D.E. Long, “Model Checking and Modular Verification,” Proc. CONCUR'91: Second Int'l Conf. Concurrency Theory, 1991.
[28] D. Harel, H. Lachover, A. Naamad, A. Pnuelli, 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, Apr. 1990.
[29] M.P.E. Heimdahl and D.J. Keenan, “Generating Code from Hierarchical State-Based Requirements,” Proc. IEEE Int'l Symp. Requirements Eng. (RE'97), Jan. 1997.
[30] C.L. Heitmeyer, B.L. Labaw, and D. Kiskis, "Consistency Checking of SCR-style Requirements Specifications," Proc. Int'l Symp. Requirements Engineering, Mar. 1995.
[31] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, "Automated Consistency Checking of Requirements Specifications," ACM Trans. Software Eng. and Methodology, pp. 231-261, vol. 5, July 1996.
[32] C.L. Heitmeyer, A. Bull, C. Gasarch, and B.G. Labaw, “SCR*: A Toolset for Specifying and Analyzing Requirements,” Proc. Conf. Computer Assurance (COMPASS), pp. 109–122, June 1995.
[33] K. Heninger, “Specifying Software Requirements for Complex Systems: New Techniques and Their Applications,” IEEE Trans. Software Eng., vol. 6, no. 1, pp. 2–12, Jan. 1980.
[34] G.J. Holzmann, “Practical Methods for Formal Validation of SDL Specifications,” Computer Comm., vol. 15, no. 2, pp. 129–134, Mar. 1992.
[35] G. Holzmann, “Designing Executable Abstractions,” Proc. Second Workshop Formal Methods in Software Practice, Mar. 1998.
[36] W.E. Howden, “Comments Analysis and Programming Errors,” IEEE Trans. Software Eng., vol. 16, no. 1, pp. 72–81, Jan. 1990.
[37] W.E. Howden and G.M. Shi, “Linear and Structural Event Sequence Analysis,” Proc. ISSTA'96, May 1996.
[38] W.E. Howden and B. Wieand, “QDA—A Method for Systematic Informal Program Analysis,” IEEE Trans. Software Eng., vol. 20, no. 6, pp. 445–462, June 1994.
[39] D. Jackson, Aspect: A Formal Specification Language for Detecting Bugs, PhD thesis, MIT, Cambridge, Mass., June 1992.
[40] D. Jackson, “Abstract Analysis with Aspect,” Proc. 1993 Int'l Symp. Software Testing and Analysis (ISSTA), pp. 19–27, June 1993.
[41] D. Jackson, “Aspect: Detecting Bugs with Abstract Dependences,” Trans. Software Eng. and Methodology, vol. 4, no. 2, pp. 109–145, Apr. 1995.
[42] D. Jackson, "Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector," Proc. ACM ISSTA'96, pp. 239-249,San Diego, 1996.
[43] J.C. Mitchell, M. Mitchell, and U. Stern, "Automated Analysis of Cryptographic Protocols Using Murφ," IEEE Symp. Security and Privacy, 1997.
[44] R.P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton Univ. Press, 1994.
[45] D.A. Lamb, Software Engineering: Planning for Change, Prentice-Hall, 1988.
[46] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[47] E. Madelaine and D. Vergamini, “Specification and Verification of a Sliding Window Protocol in LOTOS,” Proc. IFIP TC6/WG6.1 Fourth Int'l Conf. Formal Description Techniques for Distributed Systems and Comm. Protocols, pp. 495–510, Nov. 1991.
[48] W. Marrero, E. Clarke, and S. Jha, “Model Checking for Security Protocols,” Proc. DIMACS Workshop Design and Formal Verification of Security Protocols, 1997.
[49] K.L. McMillan and J. Schwalbe, “Formal Verification of the Gigamax Cache Consistency Protocol,” Shared Memory Multiprocessing, N. Suzuki, ed., MIT Press, 1992.
[50] K.M. Olender and L.J. Osterweil, “Cesar: A Static Sequencing Constraint Analyzer,” Proc. ACM SIGSOFT '89 Third Symp. Software Testing, Analysis, and Verification (TAV3), pp. 66–74, Dec. 1989.
[51] K.M. Olender and L.J. Osterweil, “Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation,” IEEE Trans. Software Eng., vol. 16, no. 3, pp. 268–280, Mar. 1990.
[52] K.M. Olender and L.K. Osterweil, “Interprocedural Static Analysis of Sequencing Constraints,” ACM Trans. Software Eng. and Methodology, vol. 1, no. 1, pp. 21–52, Jan. 1992.
[53] S. Owre, N. Shankar, and J. Rushby, “User Guide for the PVS Specification and Verification System(Draft),” technical report, Computer Science Lab, SRI Int'l, Menlo Park, Calif., 1993.
[54] D.L. Parnas and J. Madey, “Functional Documentation for Computer Systems,” Science of Computer Programming, vol. 25, no. 1, pp. 41–61, Oct. 1995.
[55] D.L. Parnas and Y. Wang, “Simulating the Behavior of Software Modules by Trace Rewriting Systems,” IEEE Trans. Software Eng., vol. 20, no. 10, pp. 750–759, 1994.
[56] D.E. Perry, “Version Control in the Inscape Environment,” Proc. Ninth Int'l Conf. Software Eng., pp. 142–149, 1987.
[57] D.E. Perry, "The Inscape Environment," Int'l Conf. Software Eng. 1989.
[58] D.E. Perry, "The Logic of Propagation in the Inscape Environment," ACM SIGSOFT, 1989.
[59] N. Shankar, “Computer-Aided Computing,” Mathematics of Program Construction, Bernhard Möller, ed., vol. 947, pp. 50–66, 1995.
[60] T. Sreemani and J.M. Atlee, "Feasibility of Model Checking Software Requirements," Proc. 11th Ann. Conf. Computer Assurance (COMPASS'96),Gaithersburg, Md., June 1996.
[61] C. Vail, “Program Verification via Abstraction using Incremental Operational Specifications,” PhD thesis, Univ. of California, San Diego, 1991.
[62] A.J. van Schouwen, “The A-7 Requirements Model: Re-examination for Real-Time Systems and an Application to Monitoring Systems,” Technical Report TR-90-276, Queen's Univ., Kingston, Ontario, May 1990.
[63] C.J. Walter, P. Lincoln, and N. Suri, “Formally Verified On-Line Diagnosis,” IEEE Trans. Software Eng., vol. 23, no. 11, pp. 684–721, Nov. 1997.
[64] W. Chan, R.J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J.D. Reese, "Model Checking Large Software Specifications," IEEE Trans. Software Eng., vol. 24, no. 7, July 1998.
[65] M.N. Wegman and K. Zadeck, “Constant Propagation,” Optimization in Compilers, F. Allen, B. Rosen, and K. Zadeck, eds., 1991.
[66] J.M. Wing and M. Vaziri-Farahani, “Model Checking Software Systems: A Case Study,” Proc. ACM SIGSOFT Symp. Foundations of Software Eng., 1995.

Index Terms:
SCR requirements, static analysis, formal specification, finite-state abstraction, data-flow analysis.
Marsha Chechik, John Gannon, "Automatic Analysis of Consistency between Requirements and Designs," IEEE Transactions on Software Engineering, vol. 27, no. 7, pp. 651-672, July 2001, doi:10.1109/32.935856
Usage of this product signifies your acceptance of the Terms of Use.