This Article 
 Bibliographic References 
 Add to: 
Completeness and Consistency in Hierarchical State-Based Requirements
June 1996 (vol. 22 no. 6)
pp. 363-377

Abstract—This paper describes methods for automatically analyzing formal, state-based requirements specifications for some aspects of completeness and consistency. The approach uses a low-level functional formalism, simplifying the analysis process. State-space explosion problems are eliminated by applying the analysis at a high level of abstraction; i.e., instead of generating a reachability graph for analysis, the analysis is performed directly on the model. The method scales up to large systems by decomposing the specification into smaller, analyzable parts and then using functional composition rules to ensure that verified properties hold for the entire specification. The analysis algorithms and tools have been validated on TCAS II, a complex, airborne, collision-avoidance system required on all commercial aircraft with more than 30 passengers that fly in U.S. airspace.

[1] J. Atlee and J. Gannon, "State-Based Model Checking of Event-Driven System Requirements," Proc. ACM SIGSOFT '91 Conf. Software for Critical Systems. Software Engineering Notes, vol. 16, No. 5, 1991.
[2] G.R. Bruns, S.L. Gerhart, I. Forman, and M. Graf, "Design Technology Assessment: The Statecharts Approach," Technical Report STP-107-86, MCC, Mar. 1986.
[3] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[4] J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill, "Symbolic Model Checking for Sequential Circuit Verification," Technical Report CMU-CS-93-211, Carnegie Mellon Univ., July 1993.
[5] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: 1020States and Beyond," Proc. IEEE Symp. Logic in Computer Science, pp. 428-439, 1990.
[6] E.M. Clarke, M.C. Browne, E.A. Emerson, and A.P. Sistla, "Using Temporal Logic for Automatic Verification of Finite State Systems," K.R. Apt, ed., Logics and Models of Concurrent Systems, pp. 3-26.Berlin: Springer-Verlag, 1985.
[7] 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.
[8] P. Godefroid, G.J. Holzmann, and D. Pirottin, "State Space Caching Revisited," Proc. Fourth Workshop Computer-Aided Verification, pp. 175-186, 1992.
[9] D. Harel, “Statecharts: A Visual Approach to Complex Systems,” Science of Computer Programming, Vol. 8, No. 3, pp. 231–274, 1987.
[10] D. Harel and A. Naamad, "The STATEMATE Semantics of StateCharts," Technical Report CS95-31, The Weizmann Institute of Science, Oct. 1995.
[11] D. Harel and A. Pnueli, "On the Development of Reactive Systems," Logic and Models of Concurrent Systems, NATO. Springer-Verlag, 1985.
[12] D. Harel, A. Pnueli, J.P. Schmidt, and R. Sherman, "On the Formal Semantics of Statecharts (extended abstract)," Proc. Second Symp. Logic in Computer Science, pp. 54-64,Ithaca, N.Y., 1987.
[13] M.P.E. Heimdahl, "Static Analysis of State-Based Requirements: Analysis for Completeness and Consistency," PhD thesis, Univ. of California, Irvine, 1994.
[14] M.P.E. Heimdahl and N.G. Leveson, "Completeness and Consistency Analysis of State-Based Requirements, Proc. 17th Int'l Conf. Software Engineering, Apr. 1995.
[15] C.L. Heitmeyer, B.L. Labaw, and D. Kiskis, "Consistency Checking of SCR-style Requirements Specifications," Proc. Int'l Symp. Requirements Engineering, Mar. 1995.
[16] K.L. Heninger, "Specifying Software for Complex Systems: New Techniques and their Application," IEEE Trans. Software Engineering, vol. 6, no. 1, pp. 2-13, Jan. 1980.
[17] K.L. Heninger, J.W. Kallander, J.E. Shore, and D.L. Parnas Software Requirements for the A-7e Aircraft. Technical Report 3876, Naval Research Laboratory, Washington, D.C., Nov. 1978.
[18] G.J. Holzmann,, "Automated Protocol Validation in Argos: Assertion Proving and Scatter Searching," IEEE Trans. Software Engineering, vol. 13, no. 6, pp. 683-696, June 1987.
[19] G.J. Holzmann, "Tracing Protocols," AT&T Technical J., vol. 64, no. 10, Dec. 1985.
[20] M.S. Jaffe, N.G. Leveson, M.P.E. Heimdahl, and B. Melhart, "Software Requirements Analysis for Real-Time Process-Control Systems," IEEE Trans. Software Engineering, vol. 17, no. 3, pp. 241-258, Mar. 1991.
[21] M.S. Jaffe, "Completeness, Robustness, and Safety in Real-Time Software Requirements and Specifications," PhD thesis, Univ. of California, Irvine, 1988.
[22] N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, and J. Reese, "TCAS II Requirements Specification,"
[23] 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.
[24] N.G. Leveson, Safeware: System Safety and Computers. Addison-Wesley, 1995.
[25] R. Lutz, "Targeting Safety-Related Errors During Software Requirements Analysis," Proc. First ACM SIGSOFT Symp.The Foundations of Software Engineering, 1993.
[26] A. Pnueli and M. Shalev, "What is in a Step?" J. Klop, J. Meijer, and J. Rutten, eds., J.W. De Baker, Liber Amicorum, pp. 373-400.CWI Amsterdam, 1989.
[27] A.P. Ravn and H. Richel, "Requirements Capture for Embedded Real-Time Systems," IMACS Symp. MCTS, 1991.
[28] H. Richel and A.P. Ravn, "Requirements Capture for Computer Based Systems," Technical Report ID/DTH HR 2/2, Technical Univ. of Denmark, Oct. 1990.
[29] J. Rushby and F. von Henke, "Formal Verification of Algorithms for Critical Systems," IEEE Trans. Software Engineering, vol. 19, no. 1, pp. 13-23, Jan. 1993.

Index Terms:
Completeness, consistency, static analysis, reactive systems, state-based requirements, formal semantics, formal methods.
Mats P.E. Heimdahl, Nancy G. Leveson, "Completeness and Consistency in Hierarchical State-Based Requirements," IEEE Transactions on Software Engineering, vol. 22, no. 6, pp. 363-377, June 1996, doi:10.1109/32.508311
Usage of this product signifies your acceptance of the Terms of Use.