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

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

E R S H I P ~ DATE. Like all attributes, this attribute can be updated. By contrast, component functions cannot be updated. If we replace the component h in the link identifier < home:h, owner:o > by a different identifier h' then the result is an identifier of a different link, not an updated link identifier. Apart from identification, L C M treats link classes in all respects in the same way as object classes. Before we turn to the formalisation of taxonomic structures, we briefly sketch the intended semantics of the specification. Formal details are given elsewhere [34,38]. 9 The specification is interpreted in a state transition system (also called a Kripke structure). 9 All states in the state space of this system have the same domain, which is the union of the ADTs presupposed by the specification. This means that all constants and operations on ADTs have the same interpretation in all states of the system; for example, it is impossible that after a state change, the meaning of integer addition would be changed. It also means that all object identifiers, which are instances of identifier types, are available in all states of the system. 9 The extension of the existence predicate may vary in different states of the system. In each state, the predicate will evaluate to true for some identifiers. Whenever an identifier is added to the extension of Exists, it is also added to the extension of Used. An identifier can only be added to the extension of Exists if it is not already in the extension of Used. Once it is in the extension of Used it is never removed from this extension. 9 Attributes are interpreted as updatable functions. In different states of the system, one attribute can be interpreted as different functions.Finally, we sketch a formalisation of subclassing. This formalisation is discussed in detail by Wieringa et al. [32]. If objects cannot migrate between subclasses of a certain class C, then the specialisation of C can be represented by a partial ordering of identifier types. For example, if Fig. 2 represents a static partitioning of TANK, then the identifier type of S T O R A G E _ T A N K is a subtype of the identifier type of TANK. This means that the sort of all TANK identifiers is partitioned by the sort of identifiers of S T O R A G E _ T A N K , M I X I N G _ TA NK and H E A T I N G _ T A N K . Because identifier types are ADTs and we use ADTs as fixed domain of all possible states of the system, this partitioning is the same in all possible states of the system, so that an identifier never changes its type; this agrees with our methodological analysis. If migration between subclasses is to remain possible, then specialisation must be formalised by means of a class predicate that can change its extension. For example, if M I X I N G T A N K is partitioned into subclasses UNASSIGNED and A S S I G N E D with the intention that mixing tanks can migrate between these two subclasses, then two predicates Unassigned and Assigned