Requirements Engineering Formal Analysis of the Shlaer-Mellor Method Towards a Toolkit of F

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

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

a collection of tools to specify software product requirements. A good example of such a toolkit for industrial product design (which is external design) is the collection of design methods described by Jones [1] in 1970. In a similar way, toolkits for software product specification are defined by Jensen and ~lbnies [2], Birrel and Ould [3] and Wieringa [4,5]. The tools that we have in mind are conceptual. They are used to reduce uncertainty about the final product by giving heuristics for making an (external) design decision and by representing the result of this decision. It is possible to supplement them with software tools such as diagram editors that take over the clerical parts of the usage of the conceptual tools..lust as in other branches of engineering, the software tools play a supporting role with respect to the usage of the conceptual tools. The toolkit approach must be contrasted approaches in which a single method is used such as SSADM or Yourdon structured analysis. In the extreme case,Formal Analysis of the Shlaer-Mellor Method107methods like these consist of a set of manuals that prescribe a _4aarticular sequence of steps in which particular m61s must be used. The advantage of a toolkit approach is that it frees the engineer from the obligation to perform tasks that are prescribed by a method but not called for by the development situation, and opens his or her mind to tools that could help to improve the quality of the final product. To get the most out of tools, our attitude towards them should be eclectic. Note that we do not advocate the abolition of method. Rather, we favour the description of the "directions for use" of requirements engineering tools in such a way that the tools can be used in different ways of working. Requirements engineering is not yet in a state where a generally accepted set of tools has been defined. There is a variety of structured analysis methods [6-10] and an even larger variety of object-oriented methods [11-J~8] that jointly offer a confusing multitude of techniques and notations. It is hard to see which techniques and notations are variants of each other and which are compatible. Putting all of these together, we most certainly do not have a coherent toolkit. The ~addition of yet another notation to the forest of techniques would not help in clarifying the situation either. Behind the syntactic differences there is a large overlap in these methods~but there are also many real differences. In order to define a usable toolkit, we have to dig behind the surface and identify a set of tools that covers the area where these methods overlap and supplement this with additional tools that are useful but do not occur in all methods. In addition, in order to increase the utility of the tools, they should resemble as much as possible the tools that software engineers are currently familiar with. This does not mean that no new tools should be defined. We think that current research in object-oriente

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

d methods has resulted in some interesting and useful additions to the more classical techniques. However, it does mean that in order to define a useful toolkit, we should not forget to include the tools that have proven their value in a number of widely used methods. In addition to claiming that we need a set of methodindependent tools that are, where possible, familiar to the software engineer, we claim that the definition of these tools should be done by formal means even if the tools themselves are semi-formal. By ensuring that semi-formal notations such as diagrams have formal counterparts, we eliminate redundancy, inconsistency, and ambiguity in the semi-formal notations and this makes them easier to use in practice. For example, we will show in this paper that the specification of object behaviour and object communication by means of diagrams can be simplified considerably if we take carethat the diagrams have precisely defined counterparts in a formal specification. This use of formal specifications does not require practitioners to ever write one letter of a formal specification, but it does demand from the tool-builders that they provide a formal theory for each tool that they produce. The situation is similar with other engineering tools: the user of a hammer does not need to have any knowledge of metallurgy or classical mechanics, but the manufacturer of a hammer does. Formal techniques not only help in the definition of conceptual tools and techniques, they also help in the definition of software tools that support the use of conceptual tools. It is one of the hallmarks of engineering that the behaviour of a product is predicted before it is implemented; this in turn requires specification of external product behaviour before the product is implemented. The conceptual tools for requirements specification are used for precisely this: to specify external product behaviour. They also should allow prediction of product properties from the specification. But this ability requires that the semi-formal notations have a formal semantics. Once we have this formal semantics, we can build software tools that allow us to predict product properties by, for example, performing reachability analysis or by animation of possible product behaviours. Backing up semi-formal notations by formal semantics therefore helps us to improve the software product engineering process. The Statemate notation and tool is a good example of this mutual enhancement of formal techniques and semi-formal notations [8,19,20]. Research in the integration of formal and semiformal techniques is scarce. Most research in this area has been done on the integration of structured analysis with formal specification techniques. France and Laro rondo-Petrie [21] give a survey. In a recent paper, Bates et al. [22] present an integration of Z with Fusion. They exclude life cycle specification from their formalisation. Feijs, Jonkers and Middelburg look at a large number of semi-forma

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

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

ict ourselves to a formal analysis of the subsystem model. Whenever we speak of "the system" below we mean the subsystem that is modelled.3. The Information Model 3.1. Structure2. The Deliverables of the Shlaer-Mellor MethodThe Shlaer-Mellor method divides the system under development into domains that each pertains to one subject matter. Each domain is inhabited by its own set of objects that behave according to a closely related set of rules and policies. For example, two domains of a railroad control system would be railroad operations and user interfaces. Domains are further divided into subsystems such that each object exists in exactly one subsystem and never moves between subsystems. Example subsystems in the domain of railroad operations are train dispatch and track management. Each subsystem is a collection of interacting objects. For each subsystem, the following models are produced.The information model in OOA uses a variant of the Entity-relationship (ER) notation. Figure 1 gives an example of the notation used in the information model. 9 Each box in the diagram represents an object class. In OOA this is called an object and instances are called object occurrences. In order to reduce the gap with other methods and prepare for the addition of this notation to our toolbox, we talk of object classes and call occurrences objects. 9 Each object class has an identifier, defined in OOA as a collection of one or more attributes whose combination always has a unique value for each instance of the class. These attributes are marked by an asterisk. 9 All relationships in the information model are binary. They are represented by bidirectional arrows. Cardinalities are one-one, many-one, or many-many, with mandatory or conditional participation on either or on both sides. A single arrowhead on one side of an arrow means exactly 1 if that side has mandatory participation, and it means 0 or 1 if that side has conditional participation. A double arrowhead on one side of an arrow means >_ 1 if that side has1. The information model shows the classes of objects that make up the subsystem, and the relationships between these object classes. The information model uses an extension of the ER notation. 2. A state model represents the behaviour of all instances of a class. State models are only specified for classes whose instances have interesting behav-Formal Analysis of the Shlaer-Mellor Method109I1. HOME [H) * Address * Unit at address9 Square feet 9 Property tax feeowns/ / / f2. ~OWNER (HO)* Owner" name,Address ownedby3. OWNERSHIP (0) * Address (R1} * Unit at address [RI]* Owner name [t:11) , Date purchasedFig 1. An associative object class. [Object Lifecycles: Modeling the World in States by Schlaer & Melior 9 1991.Reprinted by permission of Prentice-Hall Inc., Upper Saddle River, NJ.]mandatory participation and it means _ _ 0 if it has _ conditional participation. Default participation is mandatory. Conditional

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

participation is represented by the letter "c" at the arrowhead. O O A allows the definition of relationship attributes. As shown in Fig. 1, these are collected into something called an associative object class (OWNERSHIP), which is connected by an arrow to the relationship whose attributes are represented. Subclasses and superclasses are represented as shown in Fig. 2. The intention is that in each state of the system, the set of existing instances of the superclass is partitioned by the sets of existing instances of the subclasses. Each existing instance of TANK is therefore also an existing instance of exactly one of the TANK subclasses. O O A allows class migration. For example, ifMIXING_TANK would be partitioned into subclasses UNASSIGNED and ASSIGNED, we can allow amixing tank to migrate between these two subclasses.3,2. Methodological AnalysisThe information model embodies fairly standard and accepted ideas, so it is certainly a candidate for addition to our toolkit. The roots of information modelling lie in E R modelling [27] and semantic modelling [28,29]. Closely related approaches with different notational conventions can be found in other object-oriented methods, such as OMT [18] and the Coad-Yourdon method [12]. To prepare for formalisation, we analyse two important aspects of information modelling, object identification and the taxonomic hierarchy.10. TANK IT} * Tank 11399 Su~d~l (mO)RIO0~ a....IITank~D~mC~l I Heater o IR3S) 141 STORAGE TANK (S) * Tank ID [RIO0)5. MIXING TANK ~vl) * Tank ID (1:t100) 9 Mixer on/offFig 2. Representation of specialisation. [Object Lifecycles: Modeling the World in States by Schlaer & Melior @ 1991. Reprinted by permission of Prentice-Hall Inc., Upper Saddle River, NJ.]110R.J. Wieringa and G. SaakeThe importance of object identification goes beyond object-oriented requirements specification.Any administration that wants to keep track of objects in the real world must devise a way to identify these objects [30, 31]. The only way to do this is to assign a proper name to each relevant object such that there is a one-one relationship between these names and the identified objects that, once established, never changes. Thus, the set of links between proper names and identified objects grows monotonically. These proper names can then be usedas.object identifiers in the system. In order to achieve fl/is, the name must not designate any property of the object that can change. In practice, this means that the name does not carry information about the state of the object and it is indivisible, that is, it cannot be decomposed into meaningful parts. We therefore deviate from the O O A way of identifying objects and require object identifiers to be atomic. O O A rightly allows objects to migrate between classes. This has an important methodological consequence that is, however, not remarked by Shlaer and Mellor, namely that in object migration an instance may become a member of a su

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

bclass without creating an instance of a superclass [32]. For example, if an instance of M I X I N G T A N K migrates from UNASSIGNED to ASSIGNED, then the set of existing instances of UNANSIGNED is decreased by one without a change in the set of existing instances of MIXING_TANK. Contrast this with the non-migratory case: If the partitioning of TANK into S T O R A G E TANK, M I X I N G T A N K and H E A T I N G _ T A N K is static, that is migration between these subclasses is not allowed, then a change in the existence set of MIXING_TANK implies a change in the existence set of TANK. In practice, it is very difficult to find a taxonomic partition of a class that does not allow migration. For example, it is not inconceivable that the three subclasses of TANK indicate three ways of using a tank, and in that case a tank could migrate between these subclasses. Migratory and non-migratory subclassing share the property that an instance of a subclass is also an instance of the superclass. This is different in the case of role-playing, treated next. Is an E M P L O Y E E instance identical to a P E R S O N instance? At first sight, the answer seems obviously positive, until one asks whether one person can be several employees (at the same time or in series). If someone has two jobs, each with its own employee number, is this person one or two employees? If we want to keep track of the number of jobs a person has, then it may be preferable to model this person as playing two employee roles. Correspondingly, this person will have two employee identifiers and then an employee is not identical to a person. Nevertheless,there is a close relationship between employees and persons, because each employee can only exist as a role of a person. Roles can be modelled by means of a many-one relationship from E M P L O Y E E to PERSON. Summing up, the is_a arrow in an information model may represent two different situations (migratory and non-migratory subclassing) and in some cases, specialisation is more suitably modelled as role-playing, which can be represented by a many-one relationship. Any formalisation will have to take these different cases of specialisation into account.3.3. FormalisationIn this subsection, we briefly sketch a formalisation of the information model. This formalisation has been described in more detail elsewhere [33,34] but we need it here in order to understand the formalisations of the other parts of O O A specifications. The information model leaves open what the type of attributes is but in a formal specification that is counterpart of the information model, this type must be explicitly specified. We therefore assume that there is a mechanism to specify abstract data types (ADTs) and that a number of standard ADTs are available to the formal specification, such as NATURAL, STRING and MONEY. In this paper, we assume order-sorted equational logic with initial algebra semantics as the mechanism to specify ADTs. We refer to the litera

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

ture for the formal details [35-37] and here give an informal indication of what this means. 9 An A D T is a set, called a sort, with a number of operations. 9 ADTs are partially ordered to represent the subtype relation on ADTs. The subtype relation implies a subset relation on sorts. For example, in the partial ordering of number types N A T U R A L < INTEGER represents the fact that N A T U R A L is a subtype of INTEGER; this implies that the sort of naturals is a subset of the sort of integers. 9 The properties of operations are given by means of equations. For example, a property of addition on the sort N A T U R A L is that succ(n + m) = succ(n) + m, where succ is the successor function. 9 Further properties can be derived using equational logic, which is based on the substitution of equals for equals. 9 Each closed term (a term not containing variables) is the syntactic representation of a value. In the initial algebra semantics, all values are named by a closed term and different closed terms represent the same value if and only if they can be proved equal by usingFormal Analysis of the Shlaer-Mellor Method111the axioms in the specification and the rules of equational logic. We define the extension of an A D T as the set of all instances of the type in the intended semantics (in our case, in the initial algebra semantics); this is the set of all values that can be denoted by a closed term. Next, we need to formalise the concept of class. The idea is simply to formalise each attribute as a function that accepts an object identifier as argument and delivers an attribute value as result. The methodological consequence of this idea is that identifiers are themselves not attributes and that objects can never change identifiers. This agrees with our methodological analysis. In the formal specification, we now require for each object class that a corresponding identifier type has been specified, contains all identifiers that will ever be needed for objects of that class. The identifier type has the same name as the class. Each attribute is now formally declared to be a function on the identifier type of the class. For example, if we assume in Fig. 1 the name of a customer is a string, owner_name is a function H O M E O W N E R -~ S T R I N G . In any state of the system only some identifiers will identify existing objects. To single out those identifiers, we assume a predicate Exists that is applicable to all identifiers and that only evaluates to true for identifiers of existing objects. The extension of the Exists predicate is the set of identifiers for which it evaluates to true. Exists may have different extensions in different states. The existence set of a state is the set of all identifiers for which Exists evaluates to true. If Exists(n) is false for an identifier n then n may have existed in the past or it may come into existence in some possible future. If it has existed in the past, it is not available for use as identifier any

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

more. This is formalised by maintaining a unary predicate Used that is true for all identifiers that have ever been added to the existence set. The extension of this predicate is nondecreasing. Figure 3 shows an example of a formalisation of part of the information model in Fig. 1 in LCM. The specification of object class H O M E is syntactic sugar for the declaration of an identifier type H O M E and of functions address : H O M E ~ S T R I N G etc. The set of attributes {address, unit at address} is declared to be a key. This is syntactic sugar for an axiom which says that if two existing homes have the same value for this set of attributes, then they are equal:address(hi) = address(h2) and unit at address(hi) = unit at address(h2) ~" h l = h2begin object class HOME attributes address : STRING; unit at address : STRING; square_fee~ : NATURAL; property_tax fee :MONEY; keys address, unit at_address; end object class HOME; begin object class HOME_0WNEK attributes owner_name : STRING; addres : STRING; keys owner_name; end object class HOME_0WNER; begin link class OWNERSHIP components home : HOME; owner : HOME_OWNER; attributes date_purchased : DATE; end link class OWNERSHIP;Fig. 3. Specification of a relationship with attributes in LCM,where -~ stands for logical implication. Note that we formalize the identifier concept of O O A as keys in LCM. A relationship instance is a labelled tuple of component objects called a link in LCM; a relationship is called a link class in LCM. The specification of a link class must declare the components of the links. The components section of the specification of O W N E R S H I P is syntactic sugar for the specification of an identifier type whose values have the followingstructure:< home: h, owner: o > where h and o are identifiers of type H O M E and HOMEOWNER, respectively. The labels h o m e and owner in the link are the names of projection functions that retrieve the components of these identifiers. These projection functions are called component functions in LCM. Thus, we have a functionhome: O W N E R S H I P -~ H O M Edefined byh o m e (< home: h, owner: o >) = h The components section generates implicit component existence axioms such as the following:112R.J. Wieringa and G. Saakeforall os : O W N E R S H I P :: Exists(os) ~ (home(os))Exists-Cardinality constraints are formalised by placing constraints on the component functions of a link class. For example, if each existing H O M E must participate in an existing O W N E R S H I P link, then the home component function is declared to be a surjection and if each existing H O M E must participate in at most one link, then the component function home is declared to be an injection. The axioms for this are straightforward and are omitted here. Attributes applicable to relationships are formalized as functions that take link identifiers as arguments. For example, the date attribute of an O W N E R S H I P instance is a function O W N

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

E R S H I P ~ DATE. Like all attributes, this attribute can be updated. By contrast, component functions cannot be updated. If we replace the component h in the link identifier < home:h, owner:o > by a different identifier h' then the result is an identifier of a different link, not an updated link identifier. Apart from identification, L C M treats link classes in all respects in the same way as object classes. Before we turn to the formalisation of taxonomic structures, we briefly sketch the intended semantics of the specification. Formal details are given elsewhere [34,38]. 9 The specification is interpreted in a state transition system (also called a Kripke structure). 9 All states in the state space of this system have the same domain, which is the union of the ADTs presupposed by the specification. This means that all constants and operations on ADTs have the same interpretation in all states of the system; for example, it is impossible that after a state change, the meaning of integer addition would be changed. It also means that all object identifiers, which are instances of identifier types, are available in all states of the system. 9 The extension of the existence predicate may vary in different states of the system. In each state, the predicate will evaluate to true for some identifiers. Whenever an identifier is added to the extension of Exists, it is also added to the extension of Used. An identifier can only be added to the extension of Exists if it is not already in the extension of Used. Once it is in the extension of Used it is never removed from this extension. 9 Attributes are interpreted as updatable functions. In different states of the system, one attribute can be interpreted as different functions.Finally, we sketch a formalisation of subclassing. This formalisation is discussed in detail by Wieringa et al. [32]. If objects cannot migrate between subclasses of a certain class C, then the specialisation of C can be represented by a partial ordering of identifier types. For example, if Fig. 2 represents a static partitioning of TANK, then the identifier type of S T O R A G E _ T A N K is a subtype of the identifier type of TANK. This means that the sort of all TANK identifiers is partitioned by the sort of identifiers of S T O R A G E _ T A N K , M I X I N G _ TA NK and H E A T I N G _ T A N K . Because identifier types are ADTs and we use ADTs as fixed domain of all possible states of the system, this partitioning is the same in all possible states of the system, so that an identifier never changes its type; this agrees with our methodological analysis. If migration between subclasses is to remain possible, then specialisation must be formalised by means of a class predicate that can change its extension. For example, if M I X I N G T A N K is partitioned into subclasses UNASSIGNED and A S S I G N E D with the intention that mixing tanks can migrate between these two subclasses, then two predicates Unassigned and Assigned

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

are defined, whose argument is of type M I X I N G T A N K . A mixing tank would then migrate between its subclasses by changing the truth value of these class predicates. We noted earlier that role-playing can be represented by a many-one relationship with the constraint that an existing role can only be played by an existing player. This poses no special problems for the formalisation.4. The State Model 4.1. StructureFor each object class or relationship with interesting behaviour, a state model can be defined that represents the typical life cycle of class instances. The instantiation of a state model for class instances is called a state machine in OOA. Each class instance has a state attribute that indicates the current state of the object in its state machine. State models and state machines are finite state automata, which can be represented in two (equivalent) ways: the Mealy and the Moore representation, shown in Fig. 4. Both representations in the figure show a transition triggered by input event e. The transition in turn triggers output action a. In the Mealy representation a is performed during the transition and in the Moore representation, a is performed upon arrival in the destination state. Hence, in the MealyFormal Analysis of the Shlaer-Mellor Method113I$1e/at$2$1tMoore representationS2/aMealy representationFig. 4. The Mealy and Moore representationsof finite state machines.representation, output actions are attached to transitions and in the M o o r e representation, output actions are attached to states. A M o o r e representation can be transformed into an equivalent Mealy representation by moving the output action of each state to the incoming transitions of the state; conversely, a Mealy representation can be transformed into a M o o r e representation by introducing additional states in such a way that the incoming transitions of each state generate the same output actions, and then moving the output actions to the states [39,44]. The Moore representation is convenient if all transitions entering a state generate the same actions; otherwise, the M o o r e representation tends to have more states than the Mealy representation. This is illustrated by the methodological analysis below. O O A uses the Moore representation of finite state machines. A n example of a state model using the Moore representation is given in Fig. 5. Each event in a state model is an incident to which an object in the system must respond. The event may be generated by an object in the system, or it may be generated in the environment of the system. The state machine responds to an event by performing an action. O O A allows the following actions [17,45]: 9 Read or write attributes of any object in the system. 9 Perform any calculation. 9 Generate an event. This event may be received by the environment of the system, by another object, or by the object itself (in its next transition). 9 Create, delete, set, reset or read

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

a timer. A timer is an object that functions as an alarm clock. A n y number of timers may be created in the system. Relationships may have two state models, one that describes the life cycles of its instances and one, called the assigner, that monitors the creation of relationship instances. There is at most one assigner for each relationship. We ignore assigners in what follows, because they can be represented in the same way as state models that describe the life of instances.4.2. Methodological AnalysisWe will use the account state model of Fig. 5 as a vehicle to argue that an equivalent Mealy representation of the state model is considerably simpler and can be defined in such a way that it contains less implementation bias. To argue this, we start by noticing that there are two kinds of states in the account state model, stable and transitory. In a stable state of an object, the object is ready to respond to events initiated by its environment, and in a transitory state the object is busy responding to an event that it has received. When the object is busy responding to an event, it will queue incoming events so that it can respond to them later. The concept of transitory state is well known from the Ward-Mellor method of structured analysis [10]. For example, opening an account brings one into state 1, in which the M o o r e automaton creates and initialises an account and generates a deposit action. The deposit action is received by the very same object and causes transition into state 2, where the deposit is added to the balance. If the balance is non-negative, the action account OK is generated, which causes the account to move to state 3 and if the balance is negative, the action overdrawn is generated, which causes the account to move to state 4. The account then settles in state 3 or 4, that is, these are stable states in which the object can respond to events that it receives from the environment. The states that the account meets on the way are transitory. In fact, states 3 and 4 are the only stable states in the diagram. Transitory states can be used to factor out common computations among different transitions. For example, state 2 factors out the action of depositing money, which occurs in the initialisation transition of an account, in the deposit transition from the overdrawn state and in the deposit transition from the in good standing state. Transitory states m:e also useful to test a guard to determine which transition can be taken. For example, state 6 tests whether handling a check would cause the account to be overdrawn and so tests whether to go to state 7 or state 3. Let us define an object" transaction as an atomic interaction between the object and its environment,114R.J. Wieringaand G. Saakeobject, the object is in a state where either the transaction has occurred or it has not occurred. This is die classical transaction concept known from databasewhere an interaction is defined to be atomic ~{f _its inte

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

rmediary states are not observable to the environment of the object. Viewed from the environment of theACCOUntAf : Open~ [cuWa~rer arnount] ID, ICus~r1. ~sccoum~ ; h new Accourr [3. /t~count,.Ctmliartmr ID and AccourrID,=0C-,sner~ A2: Make depose (account ID, amount),a2: rv~,e ~taccourrI (~ou,~ IO, arr~ur~J l!..~.~:~.coun*=OK,acco~tlD]A99:CIo~unt[accourclD," Add ~to Account.Balance " /\ If AccotaCBelance <O, Gen=~r A6: Overdrawn A3" Acc~ mt OK (ac=~um 113] A ~se Generate A3: Accow-r OK [account II~IQ4"1IA3: A~eount OK~'~ ~ - ~ - thisJIf this is me I ~ t account forJ a U n t ID][cusl~'ner IO)tacax~lOIA4: W~drawal submitted[ac~unt ID. arnountl'! "+o-,'4/-1"" " k I I .... cnecI~"AS: C b ~ r ~ u b n ' d ~ d | (accountID. amount]5. Considering withdrawal| ~ amount <_bamnce Umn | pay check and~r~'uc.e balance by an'o.mt dise return check and reduce belen~ by bounced check fee if Account.Balance < 0 b"mn Ber-,e'~,AQ: ~ ' d r a w n (account 113) else Generate A3: ~ OK (account ~IBIIfamoum > belaace O'Bn reject ~ 1 else reduce balance by amount; end pay out; emcee Ger~-~,b= A3: AccoJrr OK (account 13)Fig 5. State models in ODA use the Moore conventi~ra.[[Object Lifecycles: Modeling the World in States by Schlaer & Melior 9 1991. Reprinted by permission of Prentice-Hall Inc., Upper Saddle River. NJ.]Formal Analysis of the Shlaer-MellorMethod115theory [40]. An object transaction is always a sequence of one or more transitions from a stable state to a stable state, moving through zero or more intermediary transitory states that are not observable from the environment. State models with the same observable behaviour but with different sequences of transitory' states are indistinguishable for the environment anc~ hence observationally equivalent. A representation of state models in which only stable states appear shows only essential object behaviour in the sense that it is free from any implementation bias [41]. Such a representation is therefore to be preferred to representations that are observationally equivalent but use different transitory states. To eliminate transitory states from a state model, we must gather all actions performed during an object transaction and compress~ them into one a e ~ n . If the object passes through a transitory state in e~zder to decide what the next stable state is going to be, tl~en the actions performed in this transitory state perform a test. In order to eliminate such a state, we must extend the labels of the arcs with guards which state the test in declarative form. This will become d e a r when we give an example in a moment. First, in order to be able to reduce the number of states of the automaton, we move from the Moore to the Mealy representation. For example, Fig. 6 shows the Mealy automaton for handling a check obtained whenwe move the action os state 6 to the incoming arc. Next, we eliminate the transitory state (number 6). Beca

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

use this state performs a test to determine if the next stable state is state 3 or state 7, we define guards which specify the condition under which, the next state is Overdrawn or In good standing. Figure 7 shows the result. The guards are added between square brackets after the event. Note that the declarative specification of the guards is less implementation-oriented than tlhe' operational specification" o f the test in Fig. 6. The Mealy model of Fig. 7 merely says which events are received, which actions are generated, and which guards must be tested by the~ object. Figure 8 sNyws the result of transforming the account' state model by moving the actions to the incoming arcs, removing transitory states and specifying guards declaratively. (The subrni~ ~heck action in state overdrawn is not present ir~.Fig. 5. We added it because there seems to be no reason to exclude it.) To summarize, the resulting Meal~ automaton illustrates three points made in the above" di~,'ussion: o Mealy automata are usually simpler than their eo/uivalent Moore automatons because they have less slates and transitions. , Because guards are~ Sl~Cified declaratively rather than operationally, they avoid implementation bias. | By the elimination of transitory states, an automaton, repJzesents essential behawiour only.3 In g o o d ~nding /checksubmittedA3If amount < b a l a n c e then p a y c h e c k and reduce b a l a n c e ~!~ a m o u n t else r e t u r n check and reduce b a l a ~ by fee If b a l a n c e <0 ~iben g e n e r a t e else g e n e r a t e A3 A6'6A67 OverdrawIFig. 6. Mealy automaton for handlii-~g a check.116R.J. Wieringa and G. Saakesubmit check(m) [balance-m <0 and balance-fee>=@] refuse_check s u b t r a ~submit check(m) [balance-m <0 and balance-fee <0] refuse check subtract feeFig. 7. Mealy automaton with declarative guard specification.!withdraw(a; m) m < balance(a)] decrease balance(a; m} ~open account(a; cid, aid) Icreate account(a; cid, aid),~OK~~ b m iI ~e_~a~ance(a;m)tcheck(a; m)submit_check(a; m) [balance-fee > 0 and m>balance(a)] refuse check(a; m) deposit(a; m) [balance(a)+m >= O] increase_balance(a; m) submit check(a; m) [balance-fee<=O m>balance(a)] and refuse check(a; m)[submit check(a; m) refuse check(a; m)deposit(a; m) [m+balance(a)>O] ~IKoI ~increase-balance(a; m)IFig. 8. Mealy autom~on with guardsin~ead G transitoG ~ e s .Formal Analysis of the Shlaer-Mellor Method117We conclude that the representation of state models without transitory states and with declarative guards is to be preferred above a representation with transitory states and guards that are specified operationally. We have no preference for the Mealy or Moore notation; indeed, in general both conventions may be mixed as in the statechart convention [8,42]. The Moore convention should be used for states for which all incoming arcs of a state generate the same action.4.3. FormalisationWhen an object t

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

ransaction occurs, a transition in the state machine of the object is taken. The following things happen in this transition: * An event that triggers the transaction is received from the environment of the object. * The guard of the transaction is evaluated. , The action associated with the transaction may cause changes in the system (OOA allows an action to have effects anywhere). 9 The action is sent to the environment of the object. The first and last items are part of the communication structure of the system and will be specified formally when we discuss the object communication model. The second and third items concern the meaning of actions (including their guards). The meaning of actions is specified in the OOA process model and we will turn to the formalisation of this part of a transition after we analyse the process model below.the attributes of the temperature ramp, and the ramp sends an event to itself to transition to the controlling state. 9 Controlling. Upon entry in the controlling state, and henceforth every time the timer expires, the ramp compares the actual cooking tank temperature with the desired temperature and turns the heater on or off accordingly. If the temperature is not high enough, the time is set to 10 seconds. If the temperature is high enough, the ramp sends an event to itself to transition to the complete state. 9 Complete. Upon entry in this state, the ramp sends an event to its environment that it is complete, turns off the heater, deletes the timer and deletes itself. Figure 10 contains an ADFD for the actions performed in the Created state. An ADFD is a collection of processes (represented by ovals) and data stores (represented by two parallel lines) connected by data flows. The processes represent operations performed during the action by objects in the system. For each process in an ADFD, a process description must be produced (not shown here). The data stores in an ADFD contain the states of existing objects of a class, called a class data store, or the states of timer objects, or the current time. There may be data stores of several different classes in one ADFD. There may be at most one data store that contains the current time. Data flows represent the flow of information in the action and are represented by arrows. Processes in one ADFD may be performed by different objects in the system. The allocation of a process to an object class is expressed by the process identifier. In Fig. 10, the following identifiers have been 9chosen: TR for Temperature Ramp, CT for Cooking Tank, and B for Batch. If the ADFD of an action in the state model of one class accesses the object data store of another class then this represents a synchronous. communication between objects of these two classes. These synchronous communications can be represented by an object access model (OAM). The OAM is a directed graph in which the nodes represent objects and the arcs processes that perform inter-object access.5. The Process

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

Model 5.1. StructureIn the process model, each action is specified by an action data flow diagram (ADFD) that represents the processing performed during the action. To illustrate this, we give an ADFD for the Created state of the temperature ramp state model in Fig. 9. The temperature ramp is part of a model Qf a controller of a juice plant that mixes juice in a cooking tank and puts it into cans. The entire model specifies the controller for the cooking tank and the canning operation and is specified more fully in Shlaer and Mellor [43]. The temperature ramp state model of Fig. 9 contains the following actions: 9 Created. Upon creation of a temperature ramp, a timer is created for this ramp, the current time and the current cooking tank temperature are stored in5.2. Methodological AnalysisThere are some problems with the use of data flow diagrams in combination with object-oriented modelling techniques. First of all, data flow diagrams represent what we call the Von Neumann partitioning principle in which data is separated from processing. This partitioning goes against the object-oriented partitioning principle that data and processing should be118R.J. Wieringaand G, Saakegrouped together [43,45]. Second, all the data in a data store is globally accessible to any process that accesses it [46]. This again contrasts with the object-orientedencapsulation of data with the processes that access it. Third, data flow diagrams specify the operations that take place during an action, and this tends to have a bias towards implementation [43,47]. To be completely free from any implementation bias, a declarative specification of the meaning of actions is to be preferred. These problems with DFDs do not imply that they should be abolished altogether. Using ideas from McMenamin and Palmer [41], we can define an essentialdata flow model of objectotransactions as a data~ flow model with the following contents (Fig. 11): 9 The state of the object is represented by a data store. 9 Each object transaction is represented~by exactly one data transformation. 9 Each data transformation represents~ exactly one object transaction.Thus, essential data transformationstt'ave no memory. We add to this McMenamin and Palmer's idea of perfect technology, which says that an essential data ftow model describes a machine with infinite processiirgTRgO: Do temperature ramp (bat:ch ID, end time, end temperature)1. Created [1] Create Temperature Ramp with an arbitrary Ramp ID and Batch ID, End Time, End Temperature from event data [2] Temperature Ramp.Timer ID := Create Timer [3] Set Temperature Ramp.Start Time = current time [4] Set Temperature Ramp.Stert Temperature = Cobking Tank.Actual Temperature [5] Generate TR11 ! S~.artcontrolling temperature (ramp id] [6] Temperature Ramp,Status - "created"TR11: ~ r ~ c, r~lling temperatura (ramp ID]..j . . . . . ..@77~13:F~mp ~imer eR~r~dIoj9. 2, Controlling..[1 ] If current time < Temperature Ramp,End Ti

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

me than Compute desired temperature at this time If Tank.Actual Temperature < desired temperature then Generate H20: Turn on heater (heater ID) else Generate H21: Turn off heater [heater ID) Generate TIMI: Set Timer (timer ID, 10 seconds. TR13. ramp ID) else Generate TR12: Complete temperetura ramp (ramp ID} [2] Set Temperature Ramp.Status - "controlling"TRl g: Campl~ temperature ramp (ramp ID]t"13. Completet[1] [2] [3] [4]Generate B91 : Temperature ramp complete [batch tO), Generate H21: Turn off heater [heater ID) Delete timer (timer tD) Delete temperature rampFig 9. State model of a temperature ramp object class. [Object Lifecycles: Modeling the World in States by Schlaer & Meli0r.~1991.Reprinted by permission of Prentice-Hall Inc., Upper Saddle River, NJ.]Formal Analysis of the Shlaer-Mellor Method119lmwer and unrestricted memory. This ties in with our earlier analysis of objeet~transactions, which are atomic anttthus conceptually take no time. It implies that there are no direct data flows between the data transformations in an essential data flow model; if there were, then the connected transformations would always be executed simultaneously (becauseiihey take no time) and hence they would represent one object transaction; but this should be represented by a single data transformatmn. Thus, 'in an essential data flow model, data transformations interface only with data stores and external entities. Figure 11 shows part of an essential data flow model for the account object class, together with a declarative specification of the two object transactions represented by the model. Inputs from the environment of theobject to a transaction are represented by data flows from an external entity to the data transformation that represents the transaction, labelled by the transaction parameters that are supplied by the external entity. Values computed by the transaction should occur as transaction parameters and are labels of output data flows to external entities. Evaluation of the guard requires data from data stores. This may involve reading from any class data store. These data flows are labelled by the attributes read from the data store. Realising the effect of the transaction involves writing to the data store of the object class to which the transaction belongs. These data flows are labelled by the attributes written to the data store. This use of data flow diagrams is in the same spirit as the functional model of the new version of OMT [48].Current Time " p.,~.=n~~~ /Batch tD + I~ndTime + End TemperatureTimer ID ~ . , ~Timer / Timer ID§ \ Start + 1 Time EndTemE~&mr~+ 19 ~"'~"~m;TiO + ]\~ ~~~"TRI 1 : Start controlling temperature {ramp IOiTemperature RampX\)Batch CookingTankT1~erature~JTemperature Ramp Fig 10. An action data flow diagram (ADFD)for the created state of the temperatureramp. [Object Lifecycles:Modelingthe World in States by Schlaer& Melior9 1991. Reprintedby permissionof

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

Prentice-HallInc., UpperSaddle River,NJ.]120R.J. Wieringa and G. SaakeACCOUNTS/curren~ala~ce+ / /urrent_stat<a, m><a, m>CUSTOMER9 increase_balance (a; m) increases the balance of a by m and sets the current state to INGOOD_STANDING if the result is non-negative.9 decrease_balance (a; m) decreases the balance of a by m only if the resulting balance would be non-negative.Fig. 11. Data flow model for two account object transactions, with declarative (informal)transaction specifications.There is a difference between OOA and other object oriented methods concerning the locality of action effects. OOA allows an action to change attribute values of any object in the system. This causes a number of problems. First, it is at odds with the object-oriented principle of encapsulation. Second, we will see below that communication is almost trivial to formalize if we require actions to have local effects only. For these reasons, we will add the restriction that an action should have local effects only. This restriction is visible in the essential data flow model of an object because the transformations in this model (which correspond to transitions in the state model) have write access only to the class data store of the object. The descriptions of the transformations should make clear that each transformation can only update the state of the object in whose life it occurs. Adding the locality restriction, this use of data flow models is perfectly compatible with object-oriented modelling. A consequence of the locality restriction is that when an action in an OOA state model has side-effects upon other objects, then this action should be split into several cooperating local actions. We return to this point when we analyse object communication below. Note that the locality restriction takes away the need to represent synchronous communication during an action in an OAM. OOA also allows the guard of a transition in a state model to be global, that is, it may test the state of any object in the system. This does not involve side-effectson other objects. The effect of evaluating the guard is purely local, namely, enabling or disabling an object transaction. We therefore follow OOA in not imposing a locality restriction on guards.5.3. ForrnalisationTo illustrate the formalisation of the process model, Fig. 12 contains a specification of the A C C O U N T object class. This specification assumes that there is a CUST O M E R object class with key attribute customer_ID that has an inverse function inv_customerID. It also assumes that a value type ACCO UNT_STATE has been specified containing only two values, O V E R D R A W N and I N _ G O O D S T A N D I N G . All possible actions of A C C O U N T objects are declared in the transitions section of the specification, shown in Fig. 13. Figure 13 shows a declarative formalisation of the guards and transactions of the A C C O U N T object class. The axioms use dynamic logic to define guards

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

and effects of transitions. There are two kinds of axioms; state axioms and transition axioms. * A state axiom is a sentence, not containing modal operators, that must be true in all states of the system. There is a state axiom in the account specification that says that the customer of an existing account must exist. Note that the customer_ ID attribute of CUSTOMER is overloaded.Formal Analysis of the Shlaer-Mellor Method9121There are two kinds of transition axioms, namely, guarding and effect axioms.- A guarding axiom has the form < a > true ~ O. This means that if the transition c~ leads to a next state, then (currently), r is true. In other words, if 0 is false, then c~ does not lead to a next state. We call the conjunction of all consequents of guarding axioms for a the guard of c~. Truth of the guard is a necessary condition for a to occur. - Effect axioms have the form r -~ [a]~. This means that if the precondition r is currently true, then after execution of a the postcondition ~p is true.Recall that in subsection 4.3, we defined the intended semantics as a state transition system in which all states share the abstract data types, including the identifier types. The states only differ in the interpretation that they give to the attribute and local predicate names of objects. This includes the Exists and Used predicates, which may have different extensions in differentpossible states. In this structure, the state axioms act as static integrity constraints that restrict the set of possible states of the system. The transition names declared in a class are interpreted as possible state transitions for the class instances. The transition axioms restrict the possible transitions that an instance can take. These axioms do not uniquely determine the possible transitions. It is for example compatible with the axioms that increase_ balance changes the customer_ID attribute of the account. It is also compatible with the axioms that if the guard of a transition is true, the transition cannot be taken: what is specified is merely that if the guard is false, the transition cannot be taken. To make the intended meaning explicit, we should state that the intended transition relation must satisfy the frame assumption and the qualification assumption. We state these assumptions informally: 9 The frame assumption says that a transition relation brings about is the smallest change compatible with the effect axioms.begin object class CUSTOMER attributes customer ID : NATURAL identifiers customer_ID; end object class CUSTOMER;inverse;begin object class ACCOUNT functions fee : MONEY; attributes account ID : NATURAL; balance : MONEY customer ID : NATURAL; current_state : ACCOUNT_STATE identifier account_ID; transitions create(ACCOUNT; account ID: NATURAL, customer ID: NATURAL) increase_balance(ACCOUNT; MONEY); decrease_balance(ACCOUNT; MONEY); accept check(ACCOUNT; MONEY); refuse_check(ACCOUNT; MONEY); state axioms --- shown in a separate fi

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

gure. transition axioms --- shown in a separate figure. end object class ACCOUNT;initially 0; initially INGOOD_STANDING;creation;Fig. 12. The CUSTOMER class has customer_lD attributes, that is unique on existing customers and that has an inverse attribute.1229R.J. Wieringa and G. SaakeThe qualification assumption says that any transitioncompatible with the guard axioms can be taken.We can summarise this by the slogan that we have a minimal change/maximal reachability semantics. It is well-known that there are different possible formalisations of minimal change and we indicate below which choices have been made in LCM. The assumptions are not expressible as first-order axioms. One way around this is to generate frame and guard sufficiency axioms for each individual specification automatically [32]. Another way of dealing with this is to translate the dynamic logic into first-order calculus, making the assumptions explicit in the translation process [49]. In both approaches, the following problems have to be dealt with.Due to the locality assumption, we know that effect axioms have only one identifier variable, which denotes the object executing the transition. However, if we would add the postcondition that for all other objects, nothing changes, then synchronous execution of several*transition would become impossible. Each transition would prohibit any synchronously executing transition from performing any change on the object that executes it, The solution to this is to apply the locality assumption only to system transactions: a system transaction ~hanges only the state of the objects that participate in"it and leaves the state of all other objects invariant. For any particular transaction, this can be expressed as first-order axioms. We return to this when we discuss system transactions.state axioms --- Staticconstraint:the customer must existf o r a l l a : ACCOUNT:: Exists(a) -> E x i s t s ( i n v _ c u s t o m e r I D ( c u s t o m e r , I D ~ a ) ) ~ ;t r a n s i t i o n axioms --- effect a x i o m for i n c r e a s e _ b a l a n c e f o r a l l a : A C C O U N T , b, m : MONEY b a l a n c e ( a ) = b and B + m >= O:: = b + m and current state=IN G00D STANDING;-> [increase_balance(a; m)] balance(a) f o r a l l a : A C C O U N T , b, m : M O N E Y :: b a l a n c e ( a ) = b and b + m < 0 -> [increase_balance(a; m)] balance(a) --- g u a r d i n g a x i o m for d e c r e a s e b a l a n c e f o r a l l a : A C C O U N T , m : MONEY :: <decrease_balance(a; m)>true -> current s t a t e = I N _ G O O D S T A N D I N G --~ effect a x i o m for decrease b a l a n c e= b + m and c u r r e n t _ s t a t e = 0 V E R D R A W N ;and m <= balance(a);f o r a l l a : A C C O U N T , b, m : MONEY :: b a l a n c e ( a ) = b -> [decrease balance(a; --- g u a r d i n g a x i o m for a c c e p t _ c h e c k f o r a l l a : A C C O U N T , m : M O N E Y :: <accept_check(a; m ) > t r u e -> current_state=IN_G00D_STANDING -

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

-- effect a x i o m for a c c e p t _ c h e c k f o r a l l a : A C C O U N T , b, m : M O N E Y balance(a) = b ->m)] balance(a)= b-m;and m <= balance(a); :: m)] balance(a) = b-m;[accept_check(a;--- g u a r d i n g a x i o m for r e f u s e _ c h e c k f o r a l l a : A C C O U N T , m : MONEY :: < r e f u s e check(a; m ) > t r u e -> m > balance(a); --- effect axioms for refuse check f o r a l l a : A C C O U N T , b, m : MONEY :: b a l a n c e ( a ) = b and fee > b -> [refuse check(a; m)] balance(a) = b-fee and current state(a)=0VERDRAWN; f o r a l l a : A C C O U N T , b, m : MONEY :: b a l a n c e ( a ) = b and Fee >= b -> [refuse check(a; m)] balance(a) = b-fee and c u r r e n t _ s t a t e ( a ) = I N ~ G O G D _ S T A N D I N O ;Fig. 13. Transition axioms for the ACCOUNT object class.Formal Analysis of the Shlaer-Mellor Method1239 Within a single object, a transition axiom may change several local attributes and:predicates. The simplest assumption here is to assume that any attribute and predicate that does not occur in the postcondition remains unchanged. For example, we can add ttie axiom that increase_balance does not change the attribute customer_ID. The problem with this approach is that some transitions may imply derived updates of the object state. We have~sl, iown elsewhere how to deal with this when derivation rules have the form of Horn clauses [50]. We are currently looking at ways to generalise this approach. 9 The qualification assumption can be formalised in a simple way by conjoining~all guards of a transition and declaring these necessary as well as sufficient for a transition to be possible. This is a kind of "guard completion". The problem with this is that in a speciatisation of the class, additional guards may be specified for the transition. The solution to this is to apply guard completion only to the most specific classes, where all constraints on a transition are known. Returning to the formalisation of the OOA techniques, we remark that the state model of a class is formalised simply by introducing a state variable and updating this variable in the effect axioms. The actions performed by a state model appear as transitions in the LCM specification and the effect axioms define the effect of these actions on the local state o f t h e object. The effect axioms thus provide the essential information about object transactions as represented in the essential data flow model of these transactions. Finally, the guard axioms formalise the guards that we. added to the statemodels in our methodological analysis of Section 4. The informal specifications of object transactions such as shown in Fig. 11 are really paraphrases of the effect and guard axioms. Note that in the formalisation we do not distinguish input from output parameters of actions; this is extra information provided by the essential data flow diagram that may be useful to the programmer who.implements the transaction. This leaves the communic

本文来源：https://www.bwwdw.com/article/tur4.html