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

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