Requirements Engineering Formal Analysis of the Shlaer-Mello(4)

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

l diagram techniques, such as message sequence charts, dataflow diagrams and H O O D diagrams, and show how these can be combined with the wide-spectrum language COLD [23]. They do not analyse any existing semi-formal specification method in detail. Bourdeau and Cheng [24] show how an OMT object diagram can be given a formal semantics in the Larch specification language. They ignore the functional and dynamic model of OMT. In a previous paper, we analysed all three models of OMT [18] using the formal specification language T R O L L [25]. One of us (Wieringa) analysed entity-relationship modelling, structured analysis and JSD to define an initial version of a toolkit for conceptual modelling of software108R,J. Wieringa and G, Saakeproduct requirements [4,26]. In this paper, we analyse the Shlaer-Mellor method for object-oriented requirements specification [16,17], called object-oriented analysis (OOA) henceforth. Like OMT, OOA is well known and is described in publicly available literature. It is additionally important because it can be viewed as a further evolution of classical structured analysis for real-time systems [10] and contains notations and ideas that are familiar to users of structured analysis. OOA is therefore a good place to look for notations and techniques that are familiar to software engineers and that are useful additions to our toolkit. The structure of this paper is as follows. In Section 2, we give an overview of the deliverables of OOA. In Sections 3-6, we analyse the major deliverables of the method, the information model, the state model, the process model and the object communication model of a system. We identify the notations used, analyse these from a methodological point of view, and indicate whether and how the notations can be formalised. As the vehicle for formalisation we use a syntactically sugared version of dynamic logic called LCM (Language for Conceptual Modeling). The focus remains on the formal analysis of OOA, however. The paper is not meant to be an introduction to LCM. Section 7 concludes the paper with a summary, discussion of results and a list of some topics for further research.iour. The state model of a class contains state transition diagrams, possibly supported by state transition tables and an event list.3. The process model represents the processing done when the system receives a stimulus. The core of the process model is an action data flow diagram (ADFD) that is specified for each action in each state model and which shows which processes are performed during the action. Each of these processes must be documented by a process specification. The process model may be supplemented by a listing of all processes and the place where they are used and by an object access model (OAM), which lists all synchronous inter-object accesses that occur during any action. 4. The object communication diagram represents asynchronous messages sent among objects by means of a directed graph.We restr