In this paper, we define a number of tools that we think belong to the core of any toolkit for requirements engineers. The tools are conceptual and hence, they need precise definitions that lay down as exactly as possible what their meaning and possible us

Requirements Eng (1996) 1: 106-131 9 1996 Springer-Verlag London LimitedRequirements EngineeringFormal Analysis of the Shlaer-Mellor Method: Towards a Toolkit of Formal and Informal Requirements Specification Techniques*R.J. Wieringa a and G, Saake baFacultyof Mathematicsand ComputerScience, FreeUniversity,Amsterdam,The NetherLands; blnstitut for TechnischeInformationssysteme,Fakult&tfor Informatik, Otto-von-Guericke-Universit&tMagdeburg, Magdeburg,Germany,In this paper, we define a number o f tools that we think belong to the core of any toolkit for requirements engineers. The tools are conceptual and hence, they need precise definitions that lay down as exactly as possible what their meaning and possible use is. We argue that this definition can best be achieved by a formal specification of the tool. This means that for each semi-formal requirements engineering tool we should provide a formal specification that precisely specifies its meaning. We argue that this mutually enhances the formal and semi-formal technique: it makes formal techniques more usable and, as we will argue, at the same time simplifies the diagram-based notations. A t the same time, we believe that the tools o f the requirements engineer should, where possible, resemble the familiar semi-formal specification techniques used in practice today. In order to achieve this, we should search existing requirements specification techniques to look for a common kernel of familiar semi-formal techniques and try to provide a formalisation for these. In this paper we illustrate this approach by a formal analysis of the Shlaer-Mellor method for object-oriented requirements specification. The formal specification language used in this analysis is LCM, a language based on dynamic logic, but similar results would have been achieved by means of another language. We analyse the techniques used in the information model, state model, process model and communication model of the ShlaerMellor method, identify ambiguities and redundancies, indicate how these can be eliminated and propose a formalisation of the result. We conclude with a listing of the tools extracted from the Shlaer-Mellor method that Correspondence and offprint requests to: aFaculty of Mathematics and Computer Science, Free University, DeBoelelaan 1081a, 1011 IV, Amsterdam, The Netherlands; Email: roelw@cs.vu.nl, http://www.cs.vu.nl/-roelwwe can add to a toolkit that in addition contains L C M as formal specification technique.Keywords:Requirements specification; Object-orientedanalysis; Formal specification; Dynamic logic1. IntroductionWe view requirements engineering as the analysis of user or market needs with the aim of identifying, first, product objectives and second, externally observable product behaviour that would satisfy these objectives. We focus in this paper on techniques for the specification of required external behaviour of software products. Just as in other branches of engineering, designers need