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

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