Constance L. Heitmeyer
Abstract
This article describes a formal analysis technique, called consistency checking, for automatic detection of errors, such as type errors, nondeterminism, missing cases, and circular definitions, in requirements specifications. The technique is designed to analyze requirements specifications expressed in the SCR (Software Cost Reduction) tabular notation. As background, the SCR approach to specifying requirements is reviewed. To provide a formal semantics for the SCR notation and a foundation for consistency checking, a formal requirements model is introduced; the model represents a software system as a finite-state automation which produces externally visible outputs in response to changes in monitored environmental quantities. Results of two experiments are presented which evaluated the utility and scalability of our technique for consistency checking in real-world avionics application. The role of consistency checking during the requirements phase of software development is discussed.
- ALSPAUGH, T.A., FAULK, S.R., BRITTON, K.H., PARKER, R.A., PARNAS, D.L., AND SHORE, J.E. 1992. Software requirements for the A-7E aircraft. Tech. Rep. NRL-9194, Naval Research Laboratory, Washington, D.C.Google Scholar
- ATLEE, J.M. AND GANNON, J. 1993. State-based model checking of event-driven system requirements. IEEE Trans. Softw. Eng. 19, 1 (Jan.), 24-40. Google Scholar
- BERRY, G. AND GONTHIER, G. 1992. The Esterel synchronous programming language: Design, semantics, implementation. Sci. Comput. Program. 19, 2, 89. Google Scholar
- BHARADWAJ, R. 1996. A generalized validity checker. Tech. Rep., Naval Research Laboratory, Washington, D.C. In preparation.Google Scholar
- BOEHM, B.W. 1981. Software Engineering Economics. Prentice-Hall, Englewood Cliffs, N.J. Google Scholar
- BRYANT, R.E. 1986. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35, 8 (Aug.), 677-691. Google Scholar
- CLARKE, E.M., EMERSON, E., AND SISTLA, A. 1986. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2 (Apr.), 244-263. Google Scholar
- COURTOIS, P.-J. AND PARNAS, D.L. 1993. Documentation for safety critical software. In Proceedings of the 15th International Conference on Software Engineering (ICSE'93) (Baltimore, Md.). ACM, New York, 315-323. Google Scholar
- CROW, J., OWRE, S., RUSHBY, J., SHANKAR, N., AND SRIVAS, M. 1995. A tutorial introduction to PVS. Tech. Rep., Computer Science Laboratory, SRI International, Menlo Park, Calif. Apr. Presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques (Boca Raton, Fla.).Google Scholar
- DAI, H. AND SCOTT, C.K. 1995. AVAT, a CASE tool for software verification and validation. In Proceedings of the IEEE 7th International Workshop on Computer-Aided Software Engineering--CASE'95 (Toronto, Canada, July). IEEE, New York, 358-367. Google Scholar
- FAIRLEY, R. 1985. Software Engineering Concepts. McGraw-Hill, New York. Google Scholar
- FAULK, S.R. 1989. State determination in hard-embedded systems. Ph.D. thesis, Univ. of North Carolina, Chapel Hill, N. Carol. Google Scholar
- FAULK, S.R. 1995. Software requirements: A tutorial. Tech. Rep. NRL-7775, Naval Research Laboratory, Washington, D.C.Google Scholar
- FAULK, S.R., BRACKETT, J., WARD, P., AND KIRBY, J., JR. 1992. The CoRE method for real-time requirements. IEEE Softw. 9, 5 (Sept.), 22-33. Google Scholar
- FAULK, S.R., FINNERAN, L., KIRBY, J., JR., SHAH, S., AND SUTTON, J. 1994. Experience applying the CoRE method to the Lockheed C-130J. In Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS '94) (Gaithersburg, Md., June). IEEE, New York, 3-8.Google Scholar
- GAO. 1992. Mission critical systems: Defense attempting to address major software challenges. Tech. Rep. GAO/IMTEC-93-13, U.S. General Accounting Office, Washington, D.C. Dec.Google Scholar
- GAREY, M. R. AND JOHNSON, D.S. 1979. Computers and Intractibility: A Guide to the Theory of NP-Completeness. Freeman, New York. Google Scholar
- GRINDLEY, C. B.B. 1968. The use of decision tables within Systematics. Comput. J. 11, 2 (Aug.), 128-133.Google Scholar
- HAREL, D. 1987. Statecharts: A visual formalism for complex systems. Sci. Comput. Program. 8, 3 (June), 231-274. Google Scholar
- HEIMDAHL, M. P. E. AND LEVESON, N. 1995. Completeness and consistency analysis of statebased requirements. In Proceedings of the 17th International Conference on Software Engineering (ICSE '95) (Seattle, Wash., Apr.). ACM, New York, 3-14. Google Scholar
- HEITMEYER, C.L. 1996. Requirements specification for hybrid systems. In Proceedings of Hybrid Systems Workshop III. Lecture Notes in Computer Science, R. Alur, T. Henzinger, and E. Sontag, Eds. Springer-Verlag, Norwell, Mass. To be published.Google Scholar
- HEITMEYER, C. L. AND MANDRIOLI, D., Eds. 1996. Formal Methods for Real-Time Computing. Vol. 5, Trends in Software. John Wiley and Sons Ltd., Chichester, England. Google Scholar
- HEITMEYER, C. L. AND MCLEAN, J. 1983. Abstract requirements specifications: A new approach and its application. IEEE Trans. Softw. Eng. SE-9, 5 (Sept.), 580-589.Google Scholar
- HEITMEYER, C. L., BULL, A., GASARCH, C., AND LABAW, B. 1995a. SCR*: A toolset for specifying and analyzing requirements. In Proceedings of the l Oth Annual Conference on Computer Assurance (COMPASS '95) (Gaithersburg, Md., June). IEEE, New York, 109-122. Google Scholar
- HEITMEYER, C. L., JEFFORDS, R. D., AND LABAW, B.G. 1996. Tools for analyzing SCR-style requirements specifications: A formal foundation. Tech. Rep., Naval Research Laboratory, Washington, D.C. In preparation.Google Scholar
- HEITMEYER, C. L., LABAW, B., AND KISKIS, D. 1995b. Consistency checking of SCR-style requirements specifications. In Proceedings of RE '95: 2nd IEEE International Symposium on Requirements Engineering (York, England, Mar.). IEEE, New York, 56-63. Google Scholar
- HENINGER, K.L. 1980. Specifying software requirements for complex systems: New techniques and their application. IEEE Trans. Softw. Eng. SE-6, 1 (Jan.), 2-13.Google Scholar
- HENINGER, K., PARNAS, D. L., SHORE, J. E., AND KALLANDER, J.W. 1978. Software requirements for the A-7E aircraft. Tech. Rep. 3876, Naval Research Laboratory, Washington, D.C.Google Scholar
- HESTER, S. D., PARNAS, D. L., AND UTTER, D.F. 1981. Using documentation as a software design medium. Bell Syst. Tech. J. 60, 8 (Oct.), 1941-1977.Google Scholar
- HOOVER, D. N. AND CHEN, Z. 1995. Tablewise, a decision table tool. In Proceedings of the 1Oth Annual Conference on Computer Assurance (COMPASS '95) (Gaithersburg, Md., June). IEEE, New York, 97-108.Google Scholar
- HUGHES, M.L., SHANK, R. M., AND STEIN, E.S. 1968. Decision Tables. MDI Publications, Wayne, Pa.Google Scholar
- HURLEY, R.B. 1983. Decision Tables in Software Engineering. Van Nostrand Reinhold, New York. Google Scholar
- JAFFE, M.S., LEVESON, N.G., HEIMDAHL, M. P. E., AND MELHART, B.E. 1991. Software requirements analysis for real-time process control systems. IEEE Trans. Softw. Eng. SE-17, 3 (Mar.), 241-258. Google Scholar
- JANICKI, R. 1995. Towards a formal semantics of Parnas tables. In Proceedings of the 17th International Conference on Software Engineering (ICSE '95) (Seattle, Wash., Apr.). ACM, New York, 231-240. Google Scholar
- LANDWEHR, C.E., HEITMEYER, C. L., AND MCLEAN, J. 1984. A security model for military message systems. ACM Trans. Comput. Syst. 2, 3 (Aug.), 198-222. Google Scholar
- LEVESON, N.G., HEIMDAHL, M.P., HILDRETH, H., AND REESE, J.D. 1994. Requirements specification for process-control systems. IEEE Trans. Softw. Eng. 20, 9 (Sept.). Google Scholar
- LINCOLN, P. AND RUSHBY, J. 1993. A formally verified algorithm for interactive consistency under a hybrid fault model. Tech. Rep. SRI-CSL-93-02, Computer Science Laboratory, SRI International. Menlo Park, Calif. Mar. Google Scholar
- LUTZ, R.R. 1993. Targeting safety-related errors during software requirements analysis. In Proceedings of the 1st ACM SIGSOFT Symposium on the Foundations of Software Engineering (Los Angeles, Calif., Dec.). ACM, New York. Google Scholar
- METZNER, J. R. AND BARNES, B.H. 1977. Decision Table Languages and Systems. Academic Press, New York. Google Scholar
- MEYER, S. AND WHITE, S. 1983. Software requirements methodology and tool study for A6-E technology transfer. Tech. Rep., Grumman Aerospace Corp., Bethpage, N.Y. July.Google Scholar
- PARNAS, D.L. 1992. Tabular representation of relations. Tech. Rep. CRL-260, Telecommunications Research Institute of Ontario (TRIO), McMaster Univ., Hamilton, Ontario, Canada. Oct.Google Scholar
- PARNAS, D.L. 1993. Some theorems we should prove. In Proceedings of the 1993 International Conference on HOL Theorem Proving and Its Applications (Vancouver, British Columbia, Canada, Aug.). Lecture Notes in Computer Science, vol. 780. Springer-Verlag, Berlin, 155-162. Google Scholar
- PARNAS, D.L. 1994. Inspection of safety-critical software using program-function tables. Tech. Rep. CRL-288, Communications Research Laboratory, McMaster Univ., Hamilton, Ontario, Canada.Google Scholar
- PARNAS, D. L. AND CLEMENTS, P.C. 1986. A rational design process: How and why to fake it. IEEE Trans. Softw. Eng. SE-12, 2 (Feb.), 251-257. Google Scholar
- PARNAS, D. L. AND MADLY, J. 1995. Functional documentation for computer systems. Sci. Comput. Program. 25, 1 (Oct.), 41-61. Google Scholar
- PARNAS, D.L., ASMIS, G., AND MADLY, g. 1991. Assessment of safety-critical software in nuclear power plants. Nucl. Safety 32, 2 (Apr.-June), 189-198.Google Scholar
- PORTER, A. A. AND VOTTA, L. G., JR. 1994. An experiment to assess different defect detection methods for software requirements inspections. In Proceedings of the 16th International Conference on Software Engineering (Sorrento, Italy, May). IEEE Computer Society Press, Los Alamitos, Calif. Google Scholar
- RUSHBY, J. AND SRIVAS, M. 1993. Using PVS to prove some theorems of David Parnas. In Proceedings of the 1993 International Conference on HOL Theorem Proving and Its Applications (Vancouver, British Columbia, Canada, Aug.). Lecture Notes in Computer Science, vol. 780. Springer-Verlag, Berlin, 163-173. Google Scholar
- SMULLYAN, R.M. 1968. First-Order Logic. Springer-Verlag, New York.Google Scholar
- VAN SCHOUWEN, A.J. 1990. The A-7 requirements model: Re-examination for real-time systems and an application for monitoring systems. Tech. Rep. TR 90-276, Queen's Univ., Kingston, Ontario, Canada.Google Scholar
- VAN SCHOUWEN, A. g., PARNAS, D. L., AND MADEY, g. 1993. Documentation of requirements for computer systems. In Proceedings of RE'93: IEEE International Symposium on Requirements Engineering (San Diego, Calif., Jan.). IEEE Computer Society Press, Los Alamitos, Calif., 198-207.Google Scholar
Index Terms
- Automated consistency checking of requirements specifications
Recommendations
Consistency checking of SCR-style requirements specifications
RE '95: Proceedings of the Second IEEE International Symposium on Requirements EngineeringThe paper describes a class of formal analysis called consistency checking that mechanically checks requirements specifications, expressed in the SCR tabular notation, for application independent properties. Properties include domain coverage, type ...
Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications
Exposing inconsistencies can uncover many defects in software specifications. One approach to exposing inconsistencies analyzes two redundant specifications, one operational and the other property-based, and reports discrepancies. This paper describes a ...
Automatic analysis of requirements consistency with the B method
A consistent requirements specification is a fundamental success factor for quality software development projects. On the one hand, writing requirements in a natural language is not good for an automated conflict detection process. On the other hand, ...
Reviews
James C. Pleasant
A technique is described for automatic detection of domain-independent errors in requirements specifications expressed in the software cost reduction (SCR) tabular notation. Types of errors considered include type errors, nondeterminism, missing cases, and circular definitions. The technique, referred to as “automated consistency checking,” focuses on automating the determination of consistency of the components of each SCR table in a requirements specification. A primary motivation for the development of the method is the high cost reported for performing such checks by hand for practical systems such as the safety-critical components of the Darlington nuclear power plant in Canada. The authors report on a scaling-up of the method to handle practical applications, including two experiments in which their automated consistency checker found “significant errors…in the requirements specification of a medium-size Navy application” (errors detected after the specification had undergone comprehensive manual checks by two independent review teams). While the paper's main emphasis is on checking the consistency of specifications, the authors report on the development of a specification editor, a simulator, and a verifier that “checks SCR requirements specifications for application properties.” A further option being considered is addition of a mechanical proof system to “support both automated consistency checking and computer-assisted verification.” In addition to the paper's contribution toward automating some of the most tedious details of requirements specifications, the formal requirements model described in the paper provides a careful theoretical framework for definition of the various tables (condition tables, event tables, and mode transition tables ) used in generating consistency checks.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments