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

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