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

发布时间:2021-06-08

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

Requirements Engineering Formal Analysis of the Shlaer-Mello(14).doc 将本文的Word文档下载到电脑

精彩图片

热门精选

大家正在看

× 游客快捷下载通道(下载后可以自由复制和排版)

限时特价:7 元/份 原价:20元

支付方式:

开通VIP包月会员 特价:29元/月

注:下载文档有可能“只有目录或者内容不全”等情况,请下载之前注意辨别,如果您已付费且无法下载或内容有问题,请联系我们协助你处理。
微信:fanwen365 QQ:370150219