VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57
An OCL-Based Framework for Model Transformations
Duc-Hanh Dang1;, Martin Gogolla2
1VNU University of Engineering and Technology, Hanoi, Vietnam
2University of Bremen, Bremen, Germany
Abstract
Model transformation is an important building block for model-driven approaches. It puts forward a necessity
andachallengetospecifyandrealizemodeltransformationaswellastoensurethecorrectnessoftransformations.
ThispaperproposesanOCL-basedframeworkformodeltransformations. Theformalfoundationoftheframework
is the integration of Triple Graph Grammars and the Object Constraint Language (OCL). The OCL-based
transformation framework o ers an on-the-fly verification of model transformations and means for transformation
quality assurance.
Received 06 December 2015, revised 25 December 2015, accepted 31 December 2015
Keywords:
Model Transformation, OCL, Validation & Verification, Precondition and Postcondition, Invariant.
1. Introduction
are proposed in [8] as a similar approach for
Model transformation can be seen as the heart
of model-driven approaches [1]. Transformations
are useful for di erent goals such as (1) to
relate views of the system to each other;
(2) to reflect about a model from other domains
for an enhancement of model analysis; and
(3) to obtain a mapping between models in
di erent languages. Within such cases it is
necessary to o er methods to specify and realize
model transformation as well as to ensure the
correctness of transformations. This is really
a challenge because of the diversity of models
and transformations.
Problem. Many approaches to model
bidirectional transformations. In addition to
specificationandrealizationoftransformationsas
proposed by these works, several papers discuss
how to ensure the correctness of transformations.
In [9] the authors introduce a method to derive
Object Constraint Language (OCL) invariants
from declarative transformations like TGGs
and QVT in order to enable their verification
and analysis. The work in [10] aims to
establish a framework for transformation testing.
To the best of our knowledge, so far there
has not been any suitable approach yet to
support both specification and quality assurance
of transformations.
transformationhavebeenintroduced, assurveyed
in [2]. The works in [3, 4] o er mechanisms
for model transformations in line with the
Query/View/Transformation (QVT) standard [5].
The ideas in [6, 7] focus on the graph
transformation-based approach for unidirectional
transformations. TripleGraphGrammars(TGGs)
Contribution. (1) In this paper we focus on the
integration of TGGs and OCL as a foundation
for model transformation. Incorporating
OCL conditions in triple rules of a triple
graph grammar allows us to express better
transformations. (2) Our approach targets
both declarative and operational features
of
transformations.
Within
the
approach
a
 Corresponding author. Email: hanhdd@vnu.edu.vn
new
method
to
extract
invariants
for
TGG
42
D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57
43
transformations is introduced. (3) We propose a
a waiting period as usual.
A camera allows the
specification method of transformations and an
system to record cars running illegally in the
OCL-based framework for model transformation.
crossing during the red signal period.
We realize the approach in USE [11], a tool
with full OCL support. This o ers an on-the-fly
verification of transformations and means for
quality assurance of transformations.
Outline. The rest of this paper is structured
as follows. Section 2 motivates our work by
meansofexamples. Section3introducesaformal
foundation for specification and realization of
transformations. Section 4 proposes an OCL-
based framework for model transformations.
Section 5 explains how the framework could
o er means for transformation quality assurance.
Section 6 shows how the approach is realized in
the USE tool. Section 7 comments on related
work. The paper is closed with a conclusion and
a discussion of future work.
The example statechart (Fig. 1) shows two
basic states On and Off, reflecting whether the
system is turned on or o . There is a concurrent
decomposition of the On state. The region on the
left corresponds to the lamp state, and the region
ontherightcorrespondstothecamerastate. Each
of these regions is concurrently active. The On
state is referred to as an orthogonal state, i.e., a
composite state containing more than one region.
Note that in our specification the synchronization
betweenthetworegionscurrentlycurrentlyisnot
reflected. TheOffstate,whichdoesnothavesub-
states, is referred to as a simple state.
The example EHA is another representation of
theexamplestatechart. ThisEHAconsistsoffour
sequential automata (denoted by rectangles),
each
of
which
contains
simple
states
and
2. Motivating Example
transitions. States can be refined by concurrently
operating sequential automata, imposing a tree
We
focus
on
a
transformation
situation
structure on them.
The refinement is expressed
between
a
statechart
and
an
extended
by the dotted arrows, e.g., the On state is refined
hierarchical
automaton.
A
UML
statechart
bytwosequentialautomata. Interleveltransitions
(state
machine)
[12]
o ers
a
light-weight
in statecharts are transitions which do not respect
notation
for
describing
the
system
behavior.
the
hierarchy
of
states,
i.e.,
those
that
may
In
order
to
model-check
statecharts,
it
is
cross borderlines of states.
The EHA expresses
necessary to transform them and represent them
them using labeled transitions in the automata
in
a
mathematical
formalism
like
Extended
representing
the
lowest
composite
state
that
Hierarchical Automata (EHAs). EHAs have been
contains all the explicit source and target states
proposed in [13] as an intermediate format to
of
the
original
transition.
For
example,
the
facilitate linking new tools to a statechart-based
interlevel transition from Count2 to RedYellow
environment.
This
formalism
uses
single-
in the statechart is represented by the transition
source/single-target
transitions
(as
in
usual
from Red to RedYellow together with the label
automata),
and
forbids
interlevel
transitions.
Count2.
This
label
is
referred
as
a
source
The EHA notation is a simple formalism with
restriction.
The transition is enabled only if its
a more restricted syntax than statecharts which
source and all state in the source restriction set
nevertheless
allows
us
to
capture
the
richer
(fCount2g) are active.
The interlevel transition
formalism [13].
Figure 1 presents models for
from Off to On is represented by the similar
a trac supervisor system for a crossing of a
transition
in
the
corresponding
automaton
main road and a country road [14].
The lamp
together
with
labels
Green
and
CameraOff,
controllerprovideshigherprecedencetothemain
called a target determination.
When taking the
road as follow: If more than two cars are waiting
transition, the target and all states in the target
at the main road (this information is provided by
determination
set
(fGreen,
CameraOffg)
are
a sensor), the lamp will be switched from red
entered and become active.
to red-yellow immediately,
instead of obeying
44
D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57
Statechart of the traffic light example
Target Determination
= {Green, CameraOff}
Target Determination
= {Count0}
Source Restriction={Count2}
Extended Hierarchical Automata
(EHA)
Fig. 1: Statechart and extended hierarchical automaton for the trac light example. (adapted from [14])
The
transformation
example
motivates
3. Foundations for a Model-Driven Approach
our work with the following requirements:
(1) Specifying and realizing of transformations:
We need to o er means so that transformations
This section explains foundations for a model-
driven approach to software engineering.
could be specified and performed, as well
as source and target models could be
represented and taken as the input and output of
transformations. (2) Verifying transformations:
We need to check if there are any defects in
3.1. Graph Transformation
Definition 1 (Graphs and Morphisms). Let a
set of labels L be given. A directed, labeled graph
is a tuple G = (VG;EG;sG;tG;lvG;leG), where
a transformation.
considered as a
A transformation can be
program taking the source
 VG is a finite set of nodes (vertices),
and target model as the input and output. We
could expect several reasonable assumptions
on such a transformation model to be satisfied.
(3) Validating transformations: The aim is to
ensure a transformation is a “right” one by
executing the transformation in various scenarios
 EG  VGVG isabinaryrelationdescribing
the edges,
 sG;tG : EG ! VG are source and target
functions mapping graph edges to nodes,
and
and comparing the de facto result with the
expected outcome. The process cannot be fully
automated: The modeler has to define relevant
scenarios, so-called test cases, and then to
 lvG : VG ! L and leG : EG ! L are
functions that assign a label to a node and
an edge, respectively.
compare the obtained and expected result.
A graph is said to be empty, if the VG and EG
are empty sets.
Let
two
directed,
labeled
graphs
G
=
(VG;EG;sG;tG;lvG;leG)
and
H
=
(VH;EH;sH;tH;lvH;leH)
be
given.
A
graph
HƯỚNG DẪN DOWNLOAD TÀI LIỆU

Bước 1:Tại trang tài liệu slideshare.vn bạn muốn tải, click vào nút Download màu xanh lá cây ở phía trên.
Bước 2: Tại liên kết tải về, bạn chọn liên kết để tải File về máy tính. Tại đây sẽ có lựa chọn tải File được lưu trên slideshare.vn
Bước 3: Một thông báo xuất hiện ở phía cuối trình duyệt, hỏi bạn muốn lưu . - Nếu click vào Save, file sẽ được lưu về máy (Quá trình tải file nhanh hay chậm phụ thuộc vào đường truyền internet, dung lượng file bạn muốn tải)
Có nhiều phần mềm hỗ trợ việc download file về máy tính với tốc độ tải file nhanh như: Internet Download Manager (IDM), Free Download Manager, ... Tùy vào sở thích của từng người mà người dùng chọn lựa phần mềm hỗ trợ download cho máy tính của mình  

An OCL-Based Framework for Model Transformations

Đăng ngày | Thể loại: | Lần tải: 0 | Lần xem: 8 | Page: 16 | FileSize: 0.00 M | File type: PDF
8 lần xem

An OCL-Based Framework for Model Transformations. This paper proposes an OCL-based framework for model transformations. The formal foundation of the framework is the integration of Triple Graph Grammars and the Object Constraint Language (OCL). The OCL-based transformation framework offers an on-the-fly verification of model transformations and means for transformation quality assurance..

Nội dung

VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 An OCL-Based Framework for Model Transformations Duc-Hanh Dang1;, Martin Gogolla2 1VNU University of Engineering and Technology, Hanoi, Vietnam 2University of Bremen, Bremen, Germany Abstract Model transformation is an important building block for model-driven approaches. It puts forward a necessity andachallengetospecifyandrealizemodeltransformationaswellastoensurethecorrectnessoftransformations. ThispaperproposesanOCL-basedframeworkformodeltransformations. Theformalfoundationoftheframework is the integration of Triple Graph Grammars and the Object Constraint Language (OCL). The OCL-based transformation framework oers an on-the-fly verification of model transformations and means for transformation quality assurance. Received 06 December 2015, revised 25 December 2015, accepted 31 December 2015 Keywords: Model Transformation, OCL, Validation & Verification, Precondition and Postcondition, Invariant. 1. Introduction Model transformation can be seen as the heart of model-driven approaches [1]. Transformations are useful for dierent goals such as (1) to relate views of the system to each other; (2) to reflect about a model from other domains for an enhancement of model analysis; and (3) to obtain a mapping between models in dierent languages. Within such cases it is necessary to oer methods to specify and realize model transformation as well as to ensure the correctness of transformations. This is really a challenge because of the diversity of models and transformations. Problem. Many approaches to model transformationhavebeenintroduced, assurveyed in [2]. The works in [3, 4] oer mechanisms for model transformations in line with the Query/View/Transformation (QVT) standard [5]. The ideas in [6, 7] focus on the graph transformation-based approach for unidirectional transformations. TripleGraphGrammars(TGGs) are proposed in [8] as a similar approach for bidirectional transformations. In addition to specificationandrealizationoftransformationsas proposed by these works, several papers discuss how to ensure the correctness of transformations. In [9] the authors introduce a method to derive Object Constraint Language (OCL) invariants from declarative transformations like TGGs and QVT in order to enable their verification and analysis. The work in [10] aims to establish a framework for transformation testing. To the best of our knowledge, so far there has not been any suitable approach yet to support both specification and quality assurance of transformations. Contribution. (1) In this paper we focus on the integration of TGGs and OCL as a foundation for model transformation. Incorporating OCL conditions in triple rules of a triple graph grammar allows us to express better transformations. (2) Our approach targets both declarative and operational features of transformations. Within the approach a Corresponding author. Email: hanhdd@vnu.edu.vn new method to extract invariants for TGG 42 D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 43 transformations is introduced. (3) We propose a specification method of transformations and an OCL-based framework for model transformation. We realize the approach in USE [11], a tool with full OCL support. This oers an on-the-fly verification of transformations and means for quality assurance of transformations. Outline. The rest of this paper is structured as follows. Section 2 motivates our work by meansofexamples. Section3introducesaformal foundation for specification and realization of transformations. Section 4 proposes an OCL-based framework for model transformations. Section 5 explains how the framework could oer means for transformation quality assurance. Section 6 shows how the approach is realized in the USE tool. Section 7 comments on related work. The paper is closed with a conclusion and a discussion of future work. a waiting period as usual. A camera allows the system to record cars running illegally in the crossing during the red signal period. The example statechart (Fig. 1) shows two basic states On and Off, reflecting whether the system is turned on or o. There is a concurrent decomposition of the On state. The region on the left corresponds to the lamp state, and the region ontherightcorrespondstothecamerastate. Each of these regions is concurrently active. The On state is referred to as an orthogonal state, i.e., a composite state containing more than one region. Note that in our specification the synchronization betweenthetworegionscurrentlycurrentlyisnot reflected. TheOffstate,whichdoesnothavesub-states, is referred to as a simple state. The example EHA is another representation of theexamplestatechart. ThisEHAconsistsoffour sequential automata (denoted by rectangles), each of which contains simple states and 2. Motivating Example transitions. States can be refined by concurrently operating sequential automata, imposing a tree We focus on a transformation situation structure on them. The refinement is expressed between a statechart and an extended by the dotted arrows, e.g., the On state is refined hierarchical automaton. A UML statechart bytwosequentialautomata. Interleveltransitions (state machine) [12] oers a light-weight in statecharts are transitions which do not respect notation for describing the system behavior. the hierarchy of states, i.e., those that may In order to model-check statecharts, it is cross borderlines of states. The EHA expresses necessary to transform them and represent them them using labeled transitions in the automata in a mathematical formalism like Extended representing the lowest composite state that Hierarchical Automata (EHAs). EHAs have been contains all the explicit source and target states proposed in [13] as an intermediate format to of the original transition. For example, the facilitate linking new tools to a statechart-based interlevel transition from Count2 to RedYellow environment. This formalism uses single- in the statechart is represented by the transition source/single-target transitions (as in usual from Red to RedYellow together with the label automata), and forbids interlevel transitions. Count2. This label is referred as a source The EHA notation is a simple formalism with a more restricted syntax than statecharts which restriction. The transition is enabled only if its source and all state in the source restriction set nevertheless allows us to capture the richer (fCount2g) are active. The interlevel transition formalism [13]. Figure 1 presents models for from Off to On is represented by the similar a trac supervisor system for a crossing of a transition in the corresponding automaton main road and a country road [14]. The lamp together with labels Green and CameraOff, controllerprovideshigherprecedencetothemain called a target determination. When taking the road as follow: If more than two cars are waiting transition, the target and all states in the target at the main road (this information is provided by determination set (fGreen, CameraOffg) are a sensor), the lamp will be switched from red entered and become active. to red-yellow immediately, instead of obeying 44 D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 Statechart of the traffic light example Target Determination = {Green, CameraOff} Target Determination = {Count0} Source Restriction={Count2} Extended Hierarchical Automata (EHA) Fig. 1: Statechart and extended hierarchical automaton for the trac light example. (adapted from [14]) The transformation example motivates 3. Foundations for a Model-Driven Approach our work with the following requirements: (1) Specifying and realizing of transformations: We need to oer means so that transformations could be specified and performed, as well as source and target models could be represented and taken as the input and output of transformations. (2) Verifying transformations: We need to check if there are any defects in a transformation. A transformation can be considered as a program taking the source and target model as the input and output. We could expect several reasonable assumptions on such a transformation model to be satisfied. (3) Validating transformations: The aim is to ensure a transformation is a “right” one by executing the transformation in various scenarios and comparing the de facto result with the expected outcome. The process cannot be fully automated: The modeler has to define relevant scenarios, so-called test cases, and then to compare the obtained and expected result. This section explains foundations for a model-driven approach to software engineering. 3.1. Graph Transformation Definition 1 (Graphs and Morphisms). Let a set of labels L be given. A directed, labeled graph is a tuple G = (VG;EG;sG;tG;lvG;leG), where VG is a finite set of nodes (vertices), EG VGVG isabinaryrelationdescribing the edges, sG;tG : EG ! VG are source and target functions mapping graph edges to nodes, and lvG : VG ! L and leG : EG ! L are functions that assign a label to a node and an edge, respectively. A graph is said to be empty, if the VG and EG are empty sets. Let two directed, labeled graphs G = (VG;EG;sG;tG;lvG;leG) and H = (VH;EH;sH;tH;lvH;leH) be given. A graph D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 45 morphism f : G ! H is a pair (fV; fE), where fV : VG ! VH, fE : EG ! EH preserves sources, targets, and labels, i.e., fV sG = sH fE and fV tG = tH fE. :Statechart sc owner owner owner onState:CompState isConcurr=true name='On' container s2e:SC2EHA c2s1:S2SH eha eha:EHA owner owner onStateH:StateH name = 'On' refined lampAut:Automata G a:X p q c:Y b:Y H a1:X d:Z v s c1:Y b1:Y lampState:CompState isConcurr=false name='Lamp' container redState:CompState isConcurr=false name='Red' s2a1:St2Aut c2s2:S2SH s2a2:St2Aut name = 'Lamp' container redStateH:StateH name = 'Red' refined counterAut:Automata name = 'Red' Fig. 2: Two directed, labeled graphs G and H and a graph morphism G ! H (informally speaking, H contains G). Figure 2 shows two directed, labeled graphs G and H and a graph morphism G ! H. The Fig. 3: Triple graph for an integrated SC2EHA model. Definition 3 (Triple Graph Grammar). A triple rule tr = L ! R consists of triple graphs L and R and an injective triple morphisms tr. mapping is represented by dashed lines between the nodes and edges of G and H. Triple graph grammars (TGGs) have been proposed as a means to specify bidirectional L = (SL sL CL tL TL) tr s c t R = (SR sR CR tR TR) translations between graph languages. Integrated graphs obtained by triple derivations are called triple graphs. Definition 2 (Triple Graphs and Morphisms). Three graphs SG, CG, and TG, called source, connection, and target graph, together with two graph morphisms sG : CG ! SG and t : CG ! TG form a triple graph G = (SG sG CG ! TG). G is said to be empty, if SG, CG, and TG are empty graphs. A triple graph morphism m = (s;c;t) : G ! H between two triple graphs G = (SG sG CG ! TG) and H = (SH sH CH ! TH) consists of three graph morphisms s : SG ! SH, c : CG ! CH and t : TG ! TH such that s sG = sH c and t tG = tH c. It is injective, if the morphisms s, c and t are injective. Figure 3 shows a triple graph containing a statechart together with correspondence nodes pointing to the extended hierarchical automata (EHA). References between source and target models denote translation correspondences. An application of a triple rule tr = (s;c;t) : L ! R to a given triple graph G to yield a triple graph H consists of the following steps: Choose an occurrence of the LHS L in G by defining a triple graph morphism m = (sm;cm;tm) : L ! G, called a triple match. Glue the graph G and the RHS R according to the occurrences of L in G so that new items that are presented in R but not in L are added to G. This yields a gluing graph Z. Formally, we have m(L \ R) = G \ Z. Here, graphs can be seen as a set of items including vertices and edges. Remove the occurrence of L from Z as well as all dangling edges, i.e., all edges incident to a removed node. This yields the resulting graph H. Formally, we have H = Z nm(L). The gluing step allows us to obtain the so-called comatch morphism n = (sn;cn;tn), where sn = SR ! SH, cn = CR ! CH, and tn = TR ! TH. The induced morphisms sH : CH ! SH and tH : CH ! TH could be obtained from the comath morphism n. 46 D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 SL CL TL sm cm tm 3.2. The Object Constraint Language G = (SG SR tr s’ sn H = (SH sH CG CR c’ cn CH tH TG) TR t’ tn TH) The Object Constraint Langauge (OCL) [15] is a formal language to describe expressions on UML models, e.g., as shown in Fig. 5: A triple graph grammar is a structure TGG = (TG;S;TR) where TG includes a so-called triple type graph and a typing function mapping so-called typed graphs to the type graph, S is an initial graph, and TR = ftr1;tr2;::::;trng is a set of triple rules. Triple graph language of TGG is the set fG j G is typed by TG ^ 9 triple graph transformation S ) Gg. (1) OCL expressions, that might be object constraints or queries, do not have side eects. (2) The OCL is a typed language. Each valid (well-formed) OCL expression has a type, which is the type of the evaluated value of this expression. The type system of OCL includes basic types (e.g., Integer, Real, String, and Boolean), object types, collection types (e.g., Collection(t), Set(t), Bag(t), and Sequence(t) for describing collections of values of type t), and message types. (3) OCL is often employed for the following purposes: {new} {new} {new} {new} {new} Fig. 4: Triple rule for the SC2EHA transformation. Figure 4 is part of a triple graph grammar thatgeneratesstatechartsandcorrespondingEHA models. This rule may create a simple state of a statechart and its corresponding state of the corresponding EHA model at any time. Such an integrated triple graph is often defined by a triple derivation. Derived triple rules allows us to compute the triple graph by taking the source (target or both) model as the input. A detailed explanation of how to apply derived Fig. 5: Object model visualized by a class diagram. To specify invariants, i.e., conditions that must be true for all instances of the class in all system states. Example: -- The number of cars is -- greater than 10. context CarModel inv: self.car.size() > 10 triples is shown in SubSect. 3.5. To describe pre- and post conditions Definition 4 (Derived Triple Rules). Each triple rule tr = L ! R derives forward, backward, and integration rules as follows: on operations. -- When a car is picked up. context Rental::assignCar(cr:Car) pre self.car = null (SR s o sL CL tL TL) id c t (SR sR CR tR TR) forward rule trF (SL sL CL t o tL TR) s c id (SR sR CR tR TR) backward rule trB (SR s o sL CL t o tL TR) id c id (SR sR CR tR TR) integration rule trI post self.car = cr To describe guards within a statechart. As a query language, i.e., to query the given where id is the identify function. system state by OCL expressions. D.H. Dang, M. Gogolla / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 42–57 47 OCL expressions are developed on the basis Aninterpretationofanobjectmodelisreferred of an object model. The aim is to allow us to as a snapshot (a system state). A snapshot is to express attribute values and logic conditions constituted by objects, links, and attribute values. on the structure defined by the object model. Specifically, the object model structure is extended with an OCL algebra [16]. Definition 5 (Object Models). An object model is the structure M = (CLASS;ATTc;OPc;ASSOC;associates; roles;multiplicities;) where 1. CLASS N isasetofnamesrepresentinga setofclasses,whereN A+ isanon-empty Fig. 6: A snapshot visualized by an object diagram. set of names over alphabet A. Each class c 2 CLASS induces an object type tc 2 T. The values of the type refer to the objects of the class. 2. ATTc is the attributes of a class c 2 CLASS, defined as a set of signatures a : tc ! t, where the attribute name a is an element of N, tc 2 T is the type of class c, and t 2 T is the type of the attribute. 3. OPc is a set of signatures for user-defined operations of a class c with type tc 2 T. The signatures are of the form ! : tc t1 ::: tn ! t,where!isthenameoftheoperation, and t, t1, ... , tn are types in T. 4. ASSOC is a set of association names. (a) associates : ASSOC ! CLASS+ is a function mapping each association name to a list of participating classes. This list has at least two elements. (b) roles : ASSOC ! N+ is a function mapping each association to a list of role names. It assigns each class participating in an association a unique role name. (c) multiplicities : ASSOC ! P(N0)+ is a function mapping each association to a list of multiplicities. It assigns each class participating in an association a multiplicity. Amultiplicityisanon-emptyset of natural numbers (an element of the power set P(N0)+) dierent from f0g. 5. is a partial order on CLASS reflecting the generalization hierarchy of classes. Figure 5 visualizes an object model in the form of a UML class diagram. Definition 6 (Snapshots). A snapshot of an object model M is the structure (M) = (CLASS;ATT;ASSOC) such that: 1. For each c 2 CLASS, the finite set CLASS(c) contains all objects of class c 2 CLASS existing in the snapshot: CLASS(c) oid(c). 2. Functions ATT assign attribute values for each object in the state. ATT(a) : CLASS(c) ! I(t) for each a : tc ! ATT. 3. For each as 2 ASSOC, there is a set of current links: ASSOC(as) IASSOC(as). A link set must satisfy all multiplicity specifications: 8i 2 f1;:::;ng;8l 2 ASSOC(as): jfl0jl0 2 ASSOC(as) ^ (i(l0) = i(l))gj 2 i(multiplicities(as)) where I(t) is the domain of each type t 2 T. oid(c)istheobjectsofeachc 2 CLASS. The