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

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

bclass without creating an instance of a superclass [32]. For example, if an instance of M I X I N G T A N K migrates from UNASSIGNED to ASSIGNED, then the set of existing instances of UNANSIGNED is decreased by one without a change in the set of existing instances of MIXING_TANK. Contrast this with the non-migratory case: If the partitioning of TANK into S T O R A G E TANK, M I X I N G T A N K and H E A T I N G _ T A N K is static, that is migration between these subclasses is not allowed, then a change in the existence set of MIXING_TANK implies a change in the existence set of TANK. In practice, it is very difficult to find a taxonomic partition of a class that does not allow migration. For example, it is not inconceivable that the three subclasses of TANK indicate three ways of using a tank, and in that case a tank could migrate between these subclasses. Migratory and non-migratory subclassing share the property that an instance of a subclass is also an instance of the superclass. This is different in the case of role-playing, treated next. Is an E M P L O Y E E instance identical to a P E R S O N instance? At first sight, the answer seems obviously positive, until one asks whether one person can be several employees (at the same time or in series). If someone has two jobs, each with its own employee number, is this person one or two employees? If we want to keep track of the number of jobs a person has, then it may be preferable to model this person as playing two employee roles. Correspondingly, this person will have two employee identifiers and then an employee is not identical to a person. Nevertheless,there is a close relationship between employees and persons, because each employee can only exist as a role of a person. Roles can be modelled by means of a many-one relationship from E M P L O Y E E to PERSON. Summing up, the is_a arrow in an information model may represent two different situations (migratory and non-migratory subclassing) and in some cases, specialisation is more suitably modelled as role-playing, which can be represented by a many-one relationship. Any formalisation will have to take these different cases of specialisation into account.3.3. FormalisationIn this subsection, we briefly sketch a formalisation of the information model. This formalisation has been described in more detail elsewhere [33,34] but we need it here in order to understand the formalisations of the other parts of O O A specifications. The information model leaves open what the type of attributes is but in a formal specification that is counterpart of the information model, this type must be explicitly specified. We therefore assume that there is a mechanism to specify abstract data types (ADTs) and that a number of standard ADTs are available to the formal specification, such as NATURAL, STRING and MONEY. In this paper, we assume order-sorted equational logic with initial algebra semantics as the mechanism to specify ADTs. We refer to the litera