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

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

and effects of transitions. There are two kinds of axioms; state axioms and transition axioms. * A state axiom is a sentence, not containing modal operators, that must be true in all states of the system. There is a state axiom in the account specification that says that the customer of an existing account must exist. Note that the customer_ ID attribute of CUSTOMER is overloaded.Formal Analysis of the Shlaer-Mellor Method9121There are two kinds of transition axioms, namely, guarding and effect axioms.- A guarding axiom has the form < a > true ~ O. This means that if the transition c~ leads to a next state, then (currently), r is true. In other words, if 0 is false, then c~ does not lead to a next state. We call the conjunction of all consequents of guarding axioms for a the guard of c~. Truth of the guard is a necessary condition for a to occur. - Effect axioms have the form r -~ [a]~. This means that if the precondition r is currently true, then after execution of a the postcondition ~p is true.Recall that in subsection 4.3, we defined the intended semantics as a state transition system in which all states share the abstract data types, including the identifier types. The states only differ in the interpretation that they give to the attribute and local predicate names of objects. This includes the Exists and Used predicates, which may have different extensions in differentpossible states. In this structure, the state axioms act as static integrity constraints that restrict the set of possible states of the system. The transition names declared in a class are interpreted as possible state transitions for the class instances. The transition axioms restrict the possible transitions that an instance can take. These axioms do not uniquely determine the possible transitions. It is for example compatible with the axioms that increase_ balance changes the customer_ID attribute of the account. It is also compatible with the axioms that if the guard of a transition is true, the transition cannot be taken: what is specified is merely that if the guard is false, the transition cannot be taken. To make the intended meaning explicit, we should state that the intended transition relation must satisfy the frame assumption and the qualification assumption. We state these assumptions informally: 9 The frame assumption says that a transition relation brings about is the smallest change compatible with the effect axioms.begin object class CUSTOMER attributes customer ID : NATURAL identifiers customer_ID; end object class CUSTOMER;inverse;begin object class ACCOUNT functions fee : MONEY; attributes account ID : NATURAL; balance : MONEY customer ID : NATURAL; current_state : ACCOUNT_STATE identifier account_ID; transitions create(ACCOUNT; account ID: NATURAL, customer ID: NATURAL) increase_balance(ACCOUNT; MONEY); decrease_balance(ACCOUNT; MONEY); accept check(ACCOUNT; MONEY); refuse_check(ACCOUNT; MONEY); state axioms --- shown in a separate fi