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

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 -