Automated consistency checking of requirements specifications

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Automated consistency checking of requirements specifications

Full text

Pdf (404 KB)

Source

ACM Transactions on Software Engineering and Methodology (TOSEM) archive
Volume 5 , Issue 3 (July 1996) table of contents

Pages: 231 - 261

Year of Publication: 1996

ISSN:1049-331X

Authors

Constance L. Heitmeyer	Naval Research Laboratory, Code 5546, Washington, D.C
Ralph D. Jeffords	Naval Research Laboratory, Code 5546, Washington, D.C
Bruce G. Labaw	Naval Research Laboratory, Code 5546, Washington, D.C

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 38, Downloads (12 Months): 207, Citation Count: 78

Additional Information:

abstract references cited by index terms review collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/234426.234431 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	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.
	2	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]
	3	Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
	4	BHARADWAJ, R. 1996. A generalized validity checker. Tech. Rep., Naval Research Laboratory, Washington, D.C. In preparation.
	5	Barry W. Boehm, Software Engineering Economics, Prentice Hall PTR, Upper Saddle River, NJ, 1981
	6	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	7	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	8	P.-J. Courtois , D. L. Parnas, Documentation for safety critical software, Proceedings of the 15th international conference on Software Engineering, p.315-323, May 17-21, 1993, Baltimore, Maryland, United States
	9	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.).
	10	Heping Dai , C. Keith Scott, AVAT, a CASE Tool for Software Verification and Validation, Proceedings of the Seventh International Workshop on Computer-Aided Software Engineering, p.358, July 10-14, 1995
	11	Richard Fairley, Software engineering concepts, McGraw-Hill, Inc., New York, NY, 1985
	12	Stuart Roland Faulk , David Lorge Parnas, State determination in hard-embedded systems, 1989
	13	FAULK, S.R. 1995. Software requirements: A tutorial. Tech. Rep. NRL-7775, Naval Research Laboratory, Washington, D.C.
	14	Stuart Faulk , John Brackett , Paul Ward , James Kirby, Jr., The Core Method for Real-Time Requirements, IEEE Software, v.9 n.5, p.22-33, September 1992 [doi>10.1109/52.156894]
	15	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.
	16	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.
	17	Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
	18	GRINDLEY, C. B.B. 1968. The use of decision tables within Systematics. Comput. J. 11, 2 (Aug.), 128-133.
	19	David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
	20	Mats P. E. Heimdahl , Nancy G. Leveson, Completeness and consistency analysis of state-based requirements, Proceedings of the 17th international conference on Software engineering, p.3-14, April 24-28, 1995, Seattle, Washington, United States [doi>10.1145/225014.225015]
	21	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.
	22	Constance Heitmeyer , Dino Mandrioli , Politecnico Milano, Formal Methods for Real-Time Computing, John Wiley & Sons, Inc., New York, NY, 1996
	23	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.
	24	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.
	25	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.
	26	C. Heitmeyer , B. Labaw , D. Kiskis, Consistency checking of SCR-style requirements specifications, Proceedings of the Second IEEE International Symposium on Requirements Engineering, p.56, March 27-29, 1995
	27	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.
	28	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.
	29	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.
	30	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.
	31	HUGHES, M.L., SHANK, R. M., AND STEIN, E.S. 1968. Decision Tables. MDI Publications, Wayne, Pa.
	32	Richard B. Hurley, Decision Tables in Software Engineering, John Wiley & Sons, Inc., New York, NY, 1983
	33	Matthew S. Jaffe , Nancy G. Leveson , Mats P. E. Heimdahl , Bonnie E. Melhart, Software Requirements Analysis for Real-Time Process-Control Systems, IEEE Transactions on Software Engineering, v.17 n.3, p.241-258, March 1991 [doi>10.1109/32.75414]
	34	Ryszard Janicki, Towards a formal semantics of Parnas tables, Proceedings of the 17th international conference on Software engineering, p.231-240, April 24-28, 1995, Seattle, Washington, United States [doi>10.1145/225014.225036]
	35	Carl E. Landwehr , Constance L. Heitmeyer , John McLean, A security model for military message systems, ACM Transactions on Computer Systems (TOCS), v.2 n.3, p.198-222, Aug. 1984 [doi>10.1145/989.991]
	36	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]
	37	Lincoln Patrick , Rushby John, A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model, NASA Langley Technical Report Server, 1993
	38	Robyn R. Lutz, Targeting safety-related errors during software requirements analysis, Proceedings of the 1st ACM SIGSOFT symposium on Foundations of software engineering, p.99-106, December 08-10, 1993, Los Angeles, California, United States
	39	Bruce H. Barnes , John R. Metzner, Decision Table Languages and Systems, Academic Press, Inc., Orlando, FL, 1977
	40	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.
	41	PARNAS, D.L. 1992. Tabular representation of relations. Tech. Rep. CRL-260, Telecommunications Research Institute of Ontario (TRIO), McMaster Univ., Hamilton, Ontario, Canada. Oct.
	42	David Lorge Parnas, Some Theorems We Should Prove, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.155-162, August 11-13, 1993
	43	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.
	44	D L Parnas , P C Clements, A rational design process: How and why to fake it, IEEE Transactions on Software Engineering, v.12 n.2, p.251-257, Feb. 1986
	45	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]
	46	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.
	47	A. A. Porter , L. G. Votta, An experiment to assess different defect detection methods for software requirements inspections, Proceedings of the 16th international conference on Software engineering, p.103-112, May 16-21, 1994, Sorrento, Italy
	48	John M. Rushby , Mandayam K. Srivas, Using PVS to Prove Some Theorems Of David Parnas, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.163-173, August 11-13, 1993
	49	SMULLYAN, R.M. 1968. First-Order Logic. Springer-Verlag, New York.
	50	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.
	51	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.

CITED BY 78

	Constance Heitmeyer , James Kirby , Bruce Labaw, The SCR method for formally specifying, verifying, and validating requirements: tool support, Proceedings of the 19th international conference on Software engineering, p.610-611, May 17-23, 1997, Boston, Massachusetts, United States
	Mats P. E. Heimdahl , Michael W. Whalen, Reduction and slicing of hierarchical state machines, ACM SIGSOFT Software Engineering Notes, v.22 n.6, p.450-467, Nov. 1997
	Constance Heitmeyer, Using SCR to specify requirements of the BART advanced automated train control system, High integrity software, Kluwer Academic Publishers, Norwell, MA, 2001
	Jeffrey M. Thompson , Mats P. E. Heimdahl , Steven P. Miller, Specification-based prototyping for embedded systems, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.163-179, Nov. 1999
	Robert J. Hall , Andrea Zisman, Model interchange and integration for web services, ACM SIGSOFT Software Engineering Notes, v.29 n.5, September 2004
	Robert J. Hall, Specification, validation, and synthesis of email agent controllers: A case study in function rich reactive system design, Proceedings of the third workshop on Formal methods in software practice, p.13-23, August 2000, Portland, Oregon, United States
	Ralph Jeffords , Constance Heitmeyer, Automatic generation of state invariants from requirements specifications, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.56-69, Nov. 1998
	Constance Heitmeyer , James Kirby , Bruce Labaw, Applying the SCR requirements method to a weapons control panel: an experience report, Proceedings of the second workshop on Formal methods in software practice, p.92-102, March 04-05, 1998, Clearwater Beach, Florida, United States
	Tevfik Bultan, Action Language: a specification language for model checking reactive systems, Proceedings of the 22nd international conference on Software engineering, p.335-344, June 04-11, 2000, Limerick, Ireland
	R. E. Kurt Stirewalt , Laura K. Dillon, A component-based approach to building formal analysis tools, Proceedings of the 23rd International Conference on Software Engineering, p.167-176, May 12-19, 2001, Toronto, Ontario, Canada
	Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.146-162, Nov. 1999
	Jon Whittle , Johann Schumann, Generating statechart designs from scenarios, Proceedings of the 22nd international conference on Software engineering, p.314-323, June 04-11, 2000, Limerick, Ireland
	Marc K. Zimmerman , Kristina Lundqvist , Nancy Leveson, Investigating the readability of state-based formal requirements specification languages, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Pamela Zave, Classification of research efforts in requirements engineering, ACM Computing Surveys (CSUR), v.29 n.4, p.315-321, Dec. 1997
	David Y. W. Park , Jens U. Skakkebæk , Mats P. E. Heimdahl , Barbara J. Czerny , David L. Dill, Checking properties of safety critical specifications using efficient decision procedures, Proceedings of the second workshop on Formal methods in software practice, p.34-43, March 04-05, 1998, Clearwater Beach, Florida, United States
	Steven P. Miller, Specifying the mode logic of a flight guidance system in CoRE and SCR, Proceedings of the second workshop on Formal methods in software practice, p.44-53, March 04-05, 1998, Clearwater Beach, Florida, United States
	Angelo Gargantini , Angelo Morzenti, Automated deductive requirements analysis of critical systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.10 n.3, p.255-307, July 2001
	Gregor Engels , Luuk Groenewegen, Object-oriented modeling: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.103-116, June 04-11, 2000, Limerick, Ireland
	Emmanuel Letier , Axel van Lamsweerde, Deriving operational software specifications from system goals, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
	Stuart Faulk , Constance Heitmeyer, Rigorous requirements for real-time systems: evolution and application of the SCR method (tutorial), Proceedings of the 19th international conference on Software engineering, p.637-638, May 17-23, 1997, Boston, Massachusetts, United States
	Bashar Nuseibeh , Steve Easterbrook, Requirements engineering: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.35-46, June 04-11, 2000, Limerick, Ireland
	Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
	Xianghua Deng , Matthew B. Dwyer , John Hatcliff , Masaaki Mizuno, Invariant-based specification, synthesis, and verification of synchronization in concurrent programs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Andrés Silva, Requirements, domain and specifications: a viewpoint-based approach to requirements engineering, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Rex Page, Functional programming, and where you can put it, ACM SIGPLAN Notices, v.36 n.9, September 2001
	Marsha Chechik, SC(R)³: towards usability of formal methods, Proceedings of the 1998 conference of the Centre for Advanced Studies on Collaborative research, p.8, November 30-December 03, 1998, Toronto, Ontario, Canada
	Emmanuel Letier , Axel van Lamsweerde, Deriving operational software specifications from system goals, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
	Axel van Lamsweerde, Requirements engineering in the year 00: a research perspective, Proceedings of the 22nd international conference on Software engineering, p.5-19, June 04-11, 2000, Limerick, Ireland
	Martin S. Feather, Rapid Application of Lightweight Formal Methods for Consistency Analyses, IEEE Transactions on Software Engineering, v.24 n.11, p.949-959, November 1998
	Arie Gurfinkel , Benet Devereux , Marsha Chechik, Model exploration with temporal logic query checking, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
	William N. Robinson , Suzanne D. Pawlowski , Vecheslav Volkov, Requirements interaction management, ACM Computing Surveys (CSUR), v.35 n.2, p.132-190, June 2003
	M. S. Feather , A. P. Nikora , C. L. Heitmeyer , N. R. Mead, ICSE 2003 workshop on Software Engineering for High Assurance Systems: synergies between process, product, and profiling (SEHAS 2003), Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	Elizabeth I. Leonard , Constance L. Heitmeyer, Program Synthesis from Formal Requirements Specifications Using APTS, Higher-Order and Symbolic Computation, v.16 n.1-2, p.63-92, March-June 2003
	Mats P. E. Heimdahl , Jeffrey M. Thompson , Barbara J. Czerny, Specification and Analysis of Intercomponent Communication, Computer, v.31 n.4, p.47-54, April 1998
	Tevfik Bultan , Richard Gerber , Christopher League, Verifying systems with integer constraints and Boolean predicates: a composite approach, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.113-123, March 1998
	Tevfik Bultan , Richard Gerber , Christopher League, Composite model-checking: verification with type-specific symbolic representations, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.3-50, Jan. 2000
	Nancy G. Leveson , Mats P. E. Heimdahl , Jon Damon Reese, Designing specification languages for process control systems: lessons learned and steps to the future, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.127-145, Nov. 1999
	Bashar Nuseibeh, Towards a framework for managing inconsistency between multiple views, Joint proceedings of the second international software architecture workshop (ISAW-2) and international workshop on multiple perspectives in software development (Viewpoints '96) on SIGSOFT '96 workshops, p.184-186, October 16-18, 1996, San Francisco, California, United States
	Jeffrey J. P. Tsai , Alan Liu , Eric Juan , Avinash Sahay, Knowledge-Based Software Architectures: Acquisition, Specification, and Verification, IEEE Transactions on Knowledge and Data Engineering, v.11 n.1, p.187-201, January 1999
	Wu Guoqing , Shu Fengdi , Wang Min , Chen Weiqing, Requirements specifications checking of embedded real-time software, Journal of Computer Science and Technology, v.17 n.1, p.56-63, January 2002
	Marsha Chechik , Benet Devereux , Arie Gurfinkel, Model-checking infinite state-space systems with fine-grained abstractions using SPIN, Proceedings of the 8th international SPIN workshop on Model checking of software, p.16-36, May 2001, Toronto, Ontario, Canada
	Arie Gurfinkel , Benet Devereux , Marsha Chechik, Model exploration with temporal logic query checking, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
	Ryszard Janicki , Emil Sekerinski, Foundations of the Trace Assertion Method of Module Interface Specification, IEEE Transactions on Software Engineering, v.27 n.7, p.577-598, July 2001
	Axel van Lamsweerde , Laurent Willemet, Inferring Declarative Requirements Specifications from Operational Scenarios, IEEE Transactions on Software Engineering, v.24 n.12, p.1089-1114, December 1998
	Marsha Chechik , John Gannon, Automatic Analysis of Consistency between Requirements and Designs, IEEE Transactions on Software Engineering, v.27 n.7, p.651-672, July 2001
	Axel van Lamsweerde , Emmanual Letier , Robert Darimont, Managing Conflicts in Goal-Driven Requirements Engineering, IEEE Transactions on Software Engineering, v.24 n.11, p.908-926, November 1998
	Axel van Lamsweerde , Emmanuel Letier, Handling Obstacles in Goal-Oriented Requirements Engineering, IEEE Transactions on Software Engineering, v.26 n.10, p.978-1005, October 2000
	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
	Hyoung Seok Hong , Seung Mo Cho , Sung Deok Cha , Yong Rae Kwon, Extending the SCR Method for Real-Time Systems, Real-Time Systems, v.20 n.1, p.27-49, Jan. 2001
	Bashar Nuseibeh , Steve Easterbrook , Alessandra Russo, Leveraging Inconsistency in Software Development, Computer, v.33 n.4, p.24-29, April 2000
	Reinhard von Hanxleden , Ali Botorabi , Slawomir Kupczyk, A Codesign Approach for Safety-Critical Automotive Applications, IEEE Micro, v.18 n.5, p.66-79, September 1998
	Emmanuel Letier , Jeff Kramer , Jeff Magee , Sebastian Uchitel, Monitoring and control in scenario-based requirements analysis, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
	Dezhuang Zhang , Rance Cleaveland, Efficient temporal-logic query checking for presburger systems, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
	Ralph D. Jeffords , Constance L. Heitmeyer, A strategy for efficiently verifying requirements, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
	Monica Brockmeyer , Farnam Jahanian , Constance Heitmeyer , Elly Winner, A Flexible, Extensible Simulation Environment for Testing Real-Time Specifications, IEEE Transactions on Computers, v.49 n.11, p.1184-1201, November 2000
	Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Constance Heitmeyer, Developing safety-critical systems: the role of formal methods and tools, Proceedings of the 10th Australian workshop on Safety critical systems and software, p.95-99, August 25, 2005, Sydney, Australia
	Aditya Ghose , George Koliadis, Model eco-systems: preliminary work, Proceedings of the fifth on Asia-Pacific conference on conceptual modelling, January 01-01, 2008, Wollongong, NSW, Australia
	Constance L. Heitmeyer , Myla Archer , Elizabeth I. Leonard , John McLean, Formal specification and verification of data separation in a separation kernel for an embedded system, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
	Tom Rothamel , Yanhong A. Liu , Constance L. Heitmeyer , Elizabeth I. Leonard, Generating optimized code from SCR specifications, ACM SIGPLAN Notices, v.41 n.7, July 2006
	David Owen , Dejan Desovski , Bojan Cukic, Random testing of formal software models and induced coverage, Proceedings of the 1st international workshop on Random testing, July 20-20, 2006, Portland, Maine
	Betty H. C. Cheng , Joanne M. Atlee, Research Directions in Requirements Engineering, 2007 Future of Software Engineering, p.285-303, May 23-25, 2007
	Sebastian Uchitel , Greg Brunet , Marsha Chechik, Behaviour Model Synthesis from Properties and Scenarios, Proceedings of the 29th International Conference on Software Engineering, p.34-43, May 20-26, 2007
	Mats P. Heimdahl , Devaraj George, On the effect of test-suite reduction on automatically generated model-based tests, Automated Software Engineering, v.14 n.1, p.37-57, March 2007
	Ana Belén Barragáns Martínez , José J. Pazos Arias , Ana Fernández Vilas , Jorge García Duque , Martín López Nores , Rebeca P. Díaz Redondo , Yolanda Blanco Fernández, On the interplay between inconsistency and incompleteness in multi-perspective requirements specifications, Information and Software Technology, v.50 n.4, p.296-321, March, 2008
	Dimitra Giannakopoulou , Corina S. Pasareanu , Jamieson M. Cobleigh, Assume-Guarantee Verification of Source Code with Design-Level Assumptions, Proceedings of the 26th International Conference on Software Engineering, p.211-220, May 23-28, 2004
	Michael Breen, Statestep: A Tool for Systematic, Incremental Specification, Proceedings of the 26th International Conference on Software Engineering, p.711-712, May 23-28, 2004
	Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999
	Robert J. Hall, Explanation-Based Scenario Generation for Reactive System Models, Automated Software Engineering, v.7 n.2, p.157-177, May 2000
	Robert J. Hall, Specification, Validation, and Synthesis of Email Agent Controllers: A Case Study in Function Rich Reactive System Design, Automated Software Engineering, v.9 n.3, p.233-261, August 2002
	Myla Archer, TAME: Using PVS strategies for special-purpose theorem proving, Annals of Mathematics and Artificial Intelligence, v.29 n.1-4, p.139-181, 2000
	Steven J. Cunning , Jerzy W. Rozenblit, Automating test generation for discrete event oriented embedded systems, Journal of Intelligent and Robotic Systems, v.41 n.2-3, p.87-112, January 2005
	Aditya K. Ghose, Formal Tools for Managing Inconsistency and Change in RE, Proceedings of the 10th International Workshop on Software Specification and Design, p.171, November 05-07, 2000
	James Robertson , Connie Heitmeyer, Point/Counterpoint, IEEE Software, v.22 n.1, p.48-51, January 2005
	Kim Lauenroth , Klaus Pohl, Towards automated consistency checks of product line requirements specifications, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Emmanuel Letier , Jeff Kramer , Jeff Magee , Sebastian Uchitel, Deriving event-based transition systems from goal-oriented requirements models, Automated Software Engineering, v.15 n.2, p.175-206, June 2008
	Michele Sama , David S. Rosenblum , Zhimin Wang , Sebastian Elbaum, Model-based fault detection in context-aware adaptive applications, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	Christophe Damas , Bernard Lambeau , Francois Roucoux , Axel van Lamsweerde, Analyzing critical process models through behavior model synthesis, Proceedings of the 2009 IEEE 31st International Conference on Software Engineering, p.441-451, May 16-24, 2009

INDEX TERMS

Primary Classification:
D. Software
D.2 SOFTWARE ENGINEERING

Additional Classification:
D. Software
D.2 SOFTWARE ENGINEERING

K. Computing Milieux
K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS

General Terms:
Languages, Management, Verification

Keywords:
application-independent properties, consistency checking, formal requirements modeling, software cost reduction methodology, tabular notations

REVIEW

"James C. Pleasant : Reviewer"

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, missi more...

Collaborative Colleagues:

Constance L. Heitmeyer: colleagues

Ralph D. Jeffords: colleagues

Bruce G. Labaw: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player