Formal refinement patterns for goal-driven requirements elaboration

ABSTRACT

Requirements engineering is concerned with the identification of high-level goals to be achieved by the system envisioned, the refinement of such goals, the operationalization of goals into services and constraints, and the assignment of responsibilities for the resulting requirements to agents such as humans, devices and programs. Goal refinement and operationalization is a complex process which is not well supported by current requirements engineering technology. Ideally some form of formal support should be provided, but formal methods are difficult and costly to apply at this stage.This paper presents an approach to goal refinement and operationalization which is aimed at providing constructive formal support while hiding the underlying mathematics. The principle is to reuse generic refinement patterns from a library structured according to strengthening/weakening relationships among patterns. The patterns are once for all proved correct and complete. They can be used for guiding the refinement process or for pointing out missing elements in a refinement. The cost inherent to the use of a formal method is thus reduced significantly. Tactics are proposed to the requirements engineer for grounding pattern selection on semantic criteria.The approach is discussed in the context of the multi-paradigm language used in the KAOS method; this language has an external semantic net layer for capturing goals, constraints, agents, objects and actions together with their links, and an inner formal assertion layer that includes a real-time temporal logic for the specification of goals and constraints. Some frequent refinement patterns are high-lighted and illustrated through a variety of examples.The general principle is somewhat similar in spirit to the increasingly popular idea of design patterns, although it is grounded on a formal framework here.

REFERENCES

• And89: J. S. Anderson , S. Fickas, A proposed perspective shift: viewing specification design as a planning problem, Proceedings of the 5th international workshop on Software specification and design, p.177-184, April 1989, Pittsburgh, Pennsylvania, United States
• Ant94: Annie I. Antón , W. Michael McCracken , Colin Potts, Goal decomposition and scenario analysis in business process reengineering, Proceedings of the 6th international conference on Advanced information systems engineering, p.94-104, June 1994, Utrecht, The Netherlands
• Ast86: E. Astesiano , M. Wirsing, An introduction ASL, The IFIP TC2/WG 2.1 Working Conference on Program specification and transformation, p.343-365, June 1987, Bad To:9Ailz, Germany
• Bal82: Robert M. Balzer , Neil M. Goldman , David S. Wile, Operational specification as the basis for rapid prototyping, ACM SIGSOFT Software Engineering Notes, v.7 n.5, p.3-16, December 1982
• BGM91: Gilles Bernot , Marie Claude Gaudel , Bruno Marre, Software testing based on formal specifications: a theory and a tool, Software Engineering Journal, v.6 n.6, p.387-405, Nov. 1991
• Boe95: Barry Boehm , Prasanta Bose , Ellis Horowitz , Ming June Lee, Software requirements negotiation and renegotiation aids, Proceedings of the 17th international conference on Software engineering, p.243-253, April 24-28, 1995, Seattle, Washington, United States [doi>10.1145/225014.225037]
• Bra85: Ronald J. Brachman , Hector J. Levesque, Readings in Knowledge Representation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1985
• Dar91: Anne Dardenne , Axel van Lamsweerde , Stephen Fickas, Goal-directed requirements acquisition, Selected Papers of the Sixth International Workshop on Software Specification and Design, p.3-50, April 1993
• Dar93: Anne Dardenne , Axel van Lamsweerde , Stephen Fickas, Goal-directed requirements acquisition, Science of Computer Programming, v.20 n.1-2, p.3-50, April 1993
• Dar95: Darimont, R., "Process Support for Requirements Elaboration", PhD Thesis, Universit~ catholique de Louvain, D~pt. Ing~nierie Informatique, Louvain-la-Neuve, Belgium, 1995.
• Doug94: Jeffrey Douglas , Richard A. Kemmerer, Aslantest: a symbolic execution tool for testing Aslan formal specifications, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.15-27, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.186487]
• Dub91: Eric Dubois , Jacques Hagelstein , André Rifaut, A formal language for the requirements engineering of computer systems, From natural language processing to logic for expert systems: a logic based approach to artificial intelligence, John Wiley and Sons Ltd., Chichester, UK, 1991
• Fea87: Martin S. Feather, Language support for the specification and development of composite systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.2, p.198-234, April 1987 [doi>10.1145/22719.22947]
• Fea94: M. Feather, "Towards a Derivational Style of Distributed System Design", Automated Software Engineering 1(1), 31- 60.
• Fic92: Stephen Fickas , B. Robert Helm, Knowledge Representation and Reasoning in the Design of Composite Systems, IEEE Transactions on Software Engineering, v.18 n.6, p.470-482, June 1992 [doi>10.1109/32.142870]
• Gam95: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• Gau92: Marie-Claude Gaudel, Structuring and Modularizing Algebraic Specifications: The PLUSS Specification Language, Evolutions and Perspectives, Proceedings of the 9th Annual Symposium on Theoretical Aspects of Computer Science, p.3-18, February 13-15, 1992
• Geo95: C. George, A.E. Haxthausen, S. Hughes, R. Milne, S, Prehn, and J.S. Pedersen, The RAISE Development Method. Prentice Hall, 1995.
• Gut93: John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
• Har87: 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]
• Hek88: Sharam Hekmatpour , Darrel C. Ince, Software Prototyping, Formal Methods, and VDM, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• Jac93: M. Jackson and P. Zave, "Domain Descriptions", Proc. RE93 - 1st Intl. IEEE Symp. on Requirements Engineering, Jan. 1993,56-64.
• Jac96: Daniel Jackson , Craig A. Damon, Elements of style: analyzing a software design feature with a counterexample detector, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.239-249, May 1996
• Jon90: Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• Koy92: Ron Koymans, Specifying Message Passing and Time-Critical Systems with Temporal Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1992
• Lam95: A. Van Lamsweerde , R. Darimont , P. Massonet, Goal-directed elaboration of requirements for a meeting scheduler: problems and lessons learnt, Proceedings of the Second IEEE International Symposium on Requirements Engineering, p.194, March 27-29, 1995
• Lan95: Kevin Lano, Formal Object-Oriented Development, Springer-Verlag New York, Inc., Secaucus, NJ, 1995
• Man92: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• Mas96: Philippe Massonet , Axel Van Lamsweerde, Analogical Reuse of Requirements Frameworks, Proceedings of the 3rd IEEE International Symposium on Requirements Engineering (RE'97), p.26, January 05-08, 1997
• Mor92: Angelo Morzenti , Dino Mandrioli , Carlo Ghezzi, A model parametric real-time logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.4, p.521-573, Oct. 1992 [doi>10.1145/133233.129397]
• Myl92: John Mylopoulos , Lawrence Chung , Brian Nixon, Representing and using nonfunctional requirements: a process-oriented approach, IEEE Transactions on Software Engineering, v.18 n.6, p.488-497, June 1992
• Nil71: Nils J. Nilsson, Problem-Solving Methods in Artificial Intelligence, McGraw-Hill Pub. Co., 1971
• Nix93: B. A. Nixon, "Dealing with Performance Requirements During the Development of Information Systems", Proc. RE93 - 1st Intl. IEEE Symp. on Requirements Engineering, Jan. 1993,42-49.
• Pot91: Ben Potter , Jane Sinclair , David Till, An introduction to formal specification and Z, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• Rep89: Thomas W. Reps , Tim Teitelbaum, The synthesizer generator: a system for constructing language-based editors, Springer-Verlag New York, Inc., New York, NY, 1989
• Reu91: Howard B. Reubenstein , Richard C. Waters, The Requirements Apprentice: Automated Assistance for Requirements Acquisition, IEEE Transactions on Software Engineering, v.17 n.3, p.226-240, March 1991 [doi>10.1109/32.75413]
• Rob89: W. N. Robinson, Integrating multiple specifications using domain goals, Proceedings of the 5th international workshop on Software specification and design, p.219-226, April 1989, Pittsburgh, Pennsylvania, United States
• Sch93: A.J. van Schouwen, D.L. Pamas, and J. Madey, "Documentation of Requirements for Computer Systems", Proc. RE'93 - 1st Intl Symp. on Requirements Engineering, IEEE, 1993, 198-207.
• Zar95: Amy Moormann Zaremski , Jeannette M. Wing, Signature matching: a tool for using software libraries, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.2, p.146-170, April 1995 [doi>10.1145/210134.210179]
• Zav82: P. Zave, "An Operational Approach to Requirements Specification for Embedded Systems", IEEE Transactions on Software Engineering, vol. 8 no, 3, May 1982,250-269.
• Zave 94: P. Zave, Classification of research efforts in requirements engineering, Proceedings of the Second IEEE International Symposium on Requirements Engineering, p.214, March 27-29, 1995

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.2.1 Requirements/Specifications
          Subjects: Languages
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

General Terms:
Algorithms, Design, Languages, Security

Keywords:
design patterns, formal methods, goal-drive requirements engineering, refinement, reuse of specifications and proof