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.
- And89.J.S. Anderson and S. Fickas, "A Proposed Perspective Shift: Viewing Specification Design as a Planning Problem", Proc. IWSSD-5 - 5th Intl. Workshop on Software Specification and Design, IEEE, 1989, 177-184. Google ScholarDigital Library
- Ant94.Anton, A. I., McCracken, W. M., Potts, C., "Goal Decomposition and Scenario analysis in Business Process Engineering, CAiSE'94, LNCS 811, Springer-Verlag, pp. 94-104. Google ScholarDigital Library
- Ast86.Astesiano, E., Wirsing, M., "An introduction to ASL", Proc. IFIP WG2.1 Conf. on Program Specifications and Transformations, North-Holland, 1986. Google ScholarDigital Library
- Bal82.R.M. Balzer, N.M. Goldman, and D.S. Wile, "Operational Specification as the Basis for Rapid Prototyping", ACM SIG- SOFT Softw. Eng. Notes Vol. 7 No. 5, Dec. 1982,3-16. Google ScholarDigital Library
- BGM91.G. Bemot, M.C. Gaudel, ad B. Marre, "Software Testing Based on Formal Specifications: A Theory and a Tool", Software Engineering Journal, 1991. Google ScholarDigital Library
- Boe95.Boehm, B., Bose, P., Horowitz, E., Ming June Lee, "Software Requirements Negotiation and Renegotiation Aids: A Theory-W Based Spiral Approach", Proc. ICSE-17 - 17th Intl. Conf on Software Engineering, Seattle, 1995, pp. 243-253. Google ScholarDigital Library
- Bra85.R.J. Brachman and H.J. Levesque (eds.), Readings in Knowledge Representation, Morgan Kaufmann, 1985. Google ScholarDigital Library
- Dar91.Dardenne, A., Fickas, S., van Lamsweerde, A., "Goal- Directed Concept Acquisition in Requirements Elicitation", Proc. IWSSD-6 - 6th Intl. Workshop on Software Specification and Design, Como, 1991, 14-21. Google ScholarDigital Library
- Dar93.Dardenne, A., van Lamsweerde, A., Fickas, S., "Goal- Directed Requirements Acquisition", Science of Computer Programming, Vol. 20, 1993,3-50. Google ScholarDigital Library
- Dar95.Darimont, R., "Process Support for Requirements Elaboration", PhD Thesis, Universit~ catholique de Louvain, D~pt. Ing~nierie Informatique, Louvain-la-Neuve, Belgium, 1995.Google Scholar
- Doug94.J. Douglas and R.A. Kemmerer, "Aslantest: A Symbolic Execution Tool for Testing ASLAN Formal Specifications", Proc. ISTSTA '94- Intl. Symp. on Software Testing and Analysis, ACM Softw. Eng. Notes, 1994, 15-27. Google ScholarDigital Library
- Dub91.Dubois, E., Hagelstein, J., Rifaut, A., "A Formal Language for the Requirements Engineering of Computer Systems," in Introducing a Logic Based Approach to Artificial Intelligence, A. Thayse (Ed.), Vol. 3, Wiley, 1991, 357-433. Google ScholarDigital Library
- Fea87.M. Feather, "Language Support for the Specification and Development of Composite Systems", ACM Trans. on Programming Languages and Systems 9(2), Apr. 87, 198-234. Google ScholarDigital Library
- Fea94.M. Feather, "Towards a Derivational Style of Distributed System Design", Automated Software Engineering 1(1), 31- 60.Google ScholarCross Ref
- Fic92.S. Fickas and R. Helm, "Knowledge Representation and Reasoning in the Design of Composite Systems", IEEE Trans. on Software Engineering, June 1992, 470-482. Google ScholarDigital Library
- Gam95.Gamma, E., Helm, R., Johnson, R., Vlissides, J,, Design Patterns - Elements of Reusable Object-Oriented Software, Addison-Wesley, 1995. Google ScholarDigital Library
- Gau92.Gaudel, M.-C., "Structuring and Modularizing Algebraic Specifications: the PLUSS specification language, evolutions and perspectives", Proc. STAS'92, LNCS 557, 1992, 3-18. Google ScholarDigital Library
- Geo95.C. George, A.E. Haxthausen, S. Hughes, R. Milne, S, Prehn, and J.S. Pedersen, The RAISE Development Method. Prentice Hall, 1995.Google Scholar
- Gut93.J.V. Guttag and J.J. Horning, LARCH: Languages and Tools for Formal Specification, Springer-Verlag, 1993. Google ScholarDigital Library
- Har87.D. Harel, "Statecharts: A Visual Formalism for Complex Systems", Science of Computer Programming, vol. 8, 1987, 231-274. Google ScholarDigital Library
- Hek88.S. Hekmatpour and D. Ince, Sojiware Prototyping, Formal Methods, and VDM. Addison-Wesley, 1988. Google ScholarDigital Library
- Jac93.M. Jackson and P. Zave, "Domain Descriptions", Proc. RE93 - 1st Intl. IEEE Symp. on Requirements Engineering, Jan. 1993,56-64.Google Scholar
- Jac96.D. Jackson and C.A. Damon, "Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector", Proc. ISTA '96- Intl. Symp. on Software Testing and Analysis, ACM Softw. En.g. Notes Vol. 21 No. 3, 1996, 239-249 . Google ScholarDigital Library
- Jon90.Jones, C.B., Systematic Software using VDM, 2nd cd., Prentice Hall. 1990. Google ScholarDigital Library
- Koy92.Koymans, R., Specifying message passing and time-critical systems with temporal logic, LNCS 651, Springer-Verlag, 1992. Google ScholarDigital Library
- Lam95.van Lamsweerde, A., Darimont, R., Massonet, P., "Goal- Directed Elaboration of Requirements for a Meeting Scheduler Problems and Lessons Learned", Proc. RE 95- 2nd Int. Symp. on Requirements Engineering, York, IEEE, 1995. Google ScholarDigital Library
- Lan95.Lano, K., Formal Object-Oriented Development, Springer-Verlag, 1995. Google ScholarDigital Library
- Man92.Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, 1992. Google ScholarDigital Library
- Mas96.P. Massonet and A. van Lamsweerde, "Analogical Reuse of Requirements Frameworks", to appear in Proc. RE-97 - 3rd Int. Symp. on Requirements Engineering, 1997. Google ScholarDigital Library
- Mor92.A. Morzenti, D. Mandrioli, and C. Ghezzi, "A Model Parametric Real-Time Logic", ACM Transactions on Programming Languages and Systems, Vol. 14 No. 4, October 1992,521-573. Google ScholarDigital Library
- Myl92.Mylopoulos, J., Chung, L., Nixon, B., "Representing and Using Nonfunctional Requirements: A Process-Oriented Approach", IEEE Trans. on Software. Engineering, Vol. 18 No, 6, June 1992, pp. 483-497. Google ScholarDigital Library
- Nil71.N.J. Nilsson, Problem Solving Methods in Artificial Intelligence. McGraw Hill, 1971. Google ScholarDigital Library
- 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.Google Scholar
- Pot91.B. Potter, J, Sinclair and D. Till, An Introduction to Formal Specification and Z. Prentice Hall, 1991. Google ScholarDigital Library
- Rep89.Reps, T. and T. Teitelbaum. The Synthesizer Generator: A System for Constructing Language-Based Editors. Spnnger-Verlag, 1989. Google ScholarDigital Library
- Reu91.H.B. Reubenstein and R.C. Waters, "The Requirements Apprentice: Automated Assistance for Requirements Acquisition", IEEE Transactions on Software Engineering, Vol. 17 No. 3, March 1991,226-240. Google ScholarDigital Library
- Rob89.Robinson, W.N., "Integrating Multiple Specifications Using Domain Goals", Proc. IWSSD-5 - 5th Intl. Workshop on Sofhvare Specification and Design, IEEE, 1989,219-225. Google ScholarDigital Library
- 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.Google Scholar
- Zar95.A.M. Zaremski and J. Wing, "Signature Matching: A Tool for Using Software Libraries", ACM Trans. on Software Engineering and Methodology 4(2), April 1995, 146-170. Google ScholarDigital Library
- 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.Google Scholar
- Zave 94.Zave, P., "Classification of Research Efforts in Requirements Engineering", Proc. RE'95 - 2nd IEEE Int. Symposium on Requirements Engineering, March 1995, 214-216. Google ScholarDigital Library
Index Terms
- Formal refinement patterns for goal-driven requirements elaboration
Recommendations
Formal refinement patterns for goal-driven requirements elaboration
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 ...
An approach of requirements tracing in formal refinement
VSTTE'10: Proceedings of the Third international conference on Verified software: theories, tools, experimentsFormal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the ...
Refinement patterns for ASTD
astd is a formal and graphical language specifically defined for information system specification. Up to now, a specifier had to build an astd specification from scratch and there were no refinement techniques for stepwise construction. This paper aims ...
Comments