Presentation

Efficient Reasoning on Finite Satisfiability in UML
Class Diagrams
Azzam Maraee Victor Makarenkov Mira Balaban
Agenda
•
•
•
•
Example
Reasoning Problems
Previous works
Research Contribution
•Conclusions and Future Work
2
Motivation
Reaction
1
1..*
C hemical
substrate
has
C atalyzedReaction
1
1..*
DNASegment
DNA
1
P r otein
1
{disjoint, incomplete}
1
[Enzyme]=2* [catalyzedReaction]
Gene
catalyzed
[Chemical]  [Reaction]
Genome
2
[Enzyme]  [Protein]
Enzyme
 [catalyzedReaction] =1/2*[Enzyme]
2*[Chemical] [Chemical]
[Protein]  [Chemical]
 ½*[Protein]  ½* [Chemical]
Agenda
•
•
•
•
Background
Reasoning Problems
Previous works
Research Contribution
– Finite Satisfiability Method:
• Class Hierarchy and Generalization Set
Constraints
•Conclusions and Future Work
4
Reasoning Problems (1):
Inconsistency
• Emptiness
disjoint
5
Reasoning Problems (2):
Infinity Problem (1)
• Consider the pervious example:
1
Advisor
+advisor
Advise
2
Master
PhD
+ma
6
Infinity Problem (2)
john : Advisor
+advise
+ma
+advise
+advise
+ma
+advice
+advise
mari : Master
advise
advise
+advsie
advise
+aadvise
advise
advise
+ma
: Master
+ma
: Master
: Master
+advsie
advise
+ma
: Master
+aadvise
advise
+ma
: Master
+advsie
advise
+ma
: Master
+advise
+ma
+ma
: Master
shreen : Master
+aadvise
+advsie
+aadvise
advise
advise
advise
+ma
: Master
+ma
: Master
+ma
: Master
+advsie
advise
+ma
: Master
sami : Master
+advsie
+advise
advise
advise
+ma
: Master
+ma
rami : PhD
+aadvise
advise
+ma
+ma
: Master
+advsie
advise
+ma
jack : Master
+aadvise
advise
+advsie
advise
+ma
+ma
frank : Master
+advise
sharon : Master
+aadvise
advise
+ma
: Master
advise
advise
+ma
michael : Master
+ma
: Master
+advsie
+advsie
+aadvise
advise
advise
advise
+ma
+ma
: Master
+ma
: Master
: Master
+aadvise
advise
+ma
: Master
+aadvise +advsie
advise
+ma
: Master
advise
+ma
: Master7
+aadvise
advise
+ma
: Master
Definitions
• A legal instance of a class diagram is an
instance that satisfies all constraints.
• A class is consistent if it has a non empty
extension in some legal instance.
• A class is finitely satisfiable if it has a non
empty extension in some legal instance.
8
Relevance of Reasoning
• It is important to guarantee that models provide
a reliable support for the designed systems.
– Implementability : A class diagram is implemented
into a running system.
– Project cost: Early detection of problems.
– Used with MDA: Precise and consistent enough to be
used within MDA.
9
Reasoning Needs (2)
• Current case tools do not support
reasoning tasks.
• Need for powerful CASE tools
– with reasoning capabilities.
10
Agenda
•
•
•
•
Background
Reasoning Problems
Previous works
Research Contribution
– Finite Satisfiability Method.
• Class Hierarchy and Generalization Set
Constraints
•Conclusions and Future Work
11
Testing Finite Satisfiability
• Lenzerini and Nobili (92):
– ER diagrams without class hierarchy.
• Calvanese and Lenzerini (94):
– Extend with class hierarchy.
12
Lenzerini and Nobily (92).
Method:
• Transform cardinality constraints into an
inequalities system.
• Solve the system.
Result: The diagram is finitely satisfiable iff
the inequalities system has a solution.
R
A
min2, max2
B
min1, max1
r≥min1∙a , r≤max1∙a , r≥min2∙b , r≤max2∙b,
a, b, r>0
13
Example
d  1 r , d  1 r
1
depend
Reaction
2
d  2  r, d  2  r
14
Example
1
depend
Reaction
2
d  1 r , d  1 r
d  2  r, d  2  r
d r
d  2r
r  2r
d  0, r  0
15
Calvanese and Lenzerini (94) – Extension
with class hierarchies (1)
• Calvanese and Lenzerini extend the method of Lenzerini
and Nobily (92) to apply to schemata with class
hierarchy.
• The expansion is based on the assumption that class
extensions may overlap.
– Compound Class.
– Compound relationship:
16
Calvanese and Lenzerini (94) –
Extension with class hierarchies
(2)
Advisor,Master_Student
Advisor,PhD_Student
Advisor,Master_Student,
PhD
Advisor
17
Calvanese and Lenzerini (94) – Extension
with class hierarchies (3)
Advisor, Master,
Ph.D
Advisor
Advisor, PhD
Advisor, Master
Advisor: Master
18
Calvanese and Lenzerini (94) –
Extension with class hierarchies (2)
• For a class diagram with three classes and one
association: 12 variables and 26 inequalities
• An exponential number of variables.
19
Hardness of Finite Satisfiability
• Berardi et al (2005) showed :
Sat ( ALC )  Sat (UML)  Sat ( DLR )  EXPTIME  complete
Sat ( ALC )  EXPTIME  complete

Sat (UML )  Sat ( ALCQI )  EXPTIME  complete
• Lutz et al (2005) showed:

FSat (UML )  FSat ( ALCQI )  EXPTIME  complete
FSat (UML)  EXPTIME  complete
20
Agenda
•
•
•
•
Background
Reasoning Problems
Previous works
Research Contribution
– Finite Satisfiability Method
•Conclusions and Future Work
21
FiniteSat Algorithm
•
The FiniteSat Algorithm
•
Input: A class diagram CD with binary multiplicity constraints, class hierarchy constraints, and GS constraints.
•
Output: A linear inequality system ψCD
•
Method:
1.
For every class, association, or multiplicity constraint: create variables and inequalities according to the Lenzerini and Nobili
method.
2.
For every class hierarchy
constraint, B being the subclass with variable b and A being the super class with variable a,
extend the inequality system with the inequalities a ≥ b.
3.
For every GS constraint GS(C, C1,...Cn; Const), C being the super-class, Cis being the subclasses, and Const being the GS
constraint, extend the inequality system, as follows:
1.
Const = disjoint:
2.
Const = complete:
3.
Const = incomplete:
4.
Cons t= overlapping: Without inequality
5.
Const = disjoint, incomplete:
6.
Const = disjoint, complete:
7.
Const = overlapping, complete:
8.
Const = overlapping, incomplete:
22
The FiniteSat Algorithm
• Class hierarchy constrain
23
GS Constraints -1
• For every GS constraint GS(C, C1,...Cn;
Const):
24
GS Constraints -2
• For every GS constraint GS(C, C1,...Cn;
Const):
25
Example 1
Reaction
1
1..*
C hemical
substrate
has
1..*
DNASegment
C atalyzedReaction
1
DNA
1
P r otein
1
{disjoint, incomplete}
1
Gene
catalyzed
Reaction
1
1..*
Genome
2
Enzyme
C hemical
Reaction
1
1..*
substrate
has
has
C atalyzedReaction
1..*
DNASegment
C hemical
substrate
1
DNA
1
P r otein
C atalyzedReaction
1..*
DNASegment
1
DNA
1
P r otein
1
1
{disjoint, incomplete}
Gene
catalyzed
Genome
2
Enzyme
{disjoint, incomplete}
1
1
Gene
catalyzed
Genome
2
Enzyme
26
Example 1
Variable:
Chemical: ch ,Reaction: r, CatalyzedReaction:c, DNA: d, Potien:p,
DNASegment, dn. Genome, ge, Gene:g, Enzyme:e
Catalyzed: ca , substrate: s, include: in
1
1..*
Inequalities:
substrate
Class hierarchy constraints inequalities:
has
1
1..*
ch>=d, c>=p, dn>=g, dn>=ge, p>=e, c>=r
1
DNASegment
Gs constraints inequalities:
1
{disjoint, incomplete}
dn>g+ge
1
Multiplicity constraint inequalities:
Gene
Genome
s>=ch, s=r, c<=r, ca=e, ca=2c, in>ge, in=dn
Reaction
DNA
CatalyzedReaction
ch,r,c,d,p,dn,ge,e,ca,s,i>0
Chemical
Protein
catalyzed 2 Enzyme
27
Performance
Claim: A Class diagram CD is finitely satisfiabile iff the
inequality system ψCD is solvable. Table 1 summarizes
our results.
28
Splitting the Problem :
Hierarchy Structure
• Tree Structure.
Advisor
Master
PhD
29
Splitting the Problem:
Hierarchy Structure
• Tree Structure.
• Acyclic Structure.
Municipal _Property
Street_Sign
Car
Police_Car
Private_Car
30
Splitting the Problem:
Hierarchy Structure
• Tree Structure
• Acyclic Structure
• Graph Structure.
31
Splitting the Problem
Hierarchy Structure
GS Constraint
Tree
Without
Acyclic
With
Graph
32
FiniteSat Extension to
Qualifier
• Qualifier
A
q1 :Tq1[tq1] min ..max
1
1
…
qn:Tqn[tqn]
R
min2..max2
B
– Imposes a partitioning on the set of related instances.
– Tightens the multiplicity constraint of its association.
– Can cause finite satisfiability problems.
FiniteSat Extension to Qualifier Example
TV-Network
Day :
Weekday
1
1
WeekdaySchedule
NetworkSchedule
1
Broadcast
Schedule
1
Enum WeekDay = {Sunday, Monday, Tuesday, Wednesday, Thursday, Friday,
Saturday}
• In every legal instance
– Number of broadcast schedules, b, is 7*t, where t
is the number of TV-Networks. At the same time
t=b. The only solution for:
• b=7t
• b=t
Is empty or infinite!
FiniteSat Extension to Qualifier – General
case
• If a combined domain value is non-finite,
ignore the qualifier constraint, and handle like
regular association.
• Else, extend the inequality system with the
following inequalities:
– min1 x b <= r <= max1 x b
– min2 x a x tq1 x … x tqn <= r <= max2 x a x tq1 x
… x tqn
Exploring the Limits
• Infinity
A
disjoint
B
C
D
1
R
E
1
36
The Inequalities System
a bcd
a  isa1, a  isa 2, a  isa 3
b  isa1, c  isa 2, d  isa 3
e  isa 4, e  isa5
c  isa 4, d  isa5
ecd
There is a solution
37
38
Future Work
• Extensions:
– Graph structure with disjoint, complete.
– N-ary.
– Aggregation.
– Identification and Fixing (Sven Hartman,
2001)
– integrate the implementation as add-in in
existing case tool,
39
40
Backup Slides
41
Finite Satisfiabilty over Unconstrained Tree
Hierarchy
A class diagram
that includes binary
Class Diagram
Create the Lenzerini
associations and
without hierarchy
& Nobili inequalities
unconstrained tree
constraint
system and Solve.
hierarchy
super 1 1 super
ISA1
ISA2
0..1
0..1
sub
sub
42
Finite Satisfiabilty over Unconstrained Tree Hierarchy
Claims
• Claim [correctness]: A class diagram with
unconstrained tree hierarchy is finitely satisfiable
iff there exists a solution to the inequalities system.
• Claim [Complexity]: Unconstrained Tree Hierarchy
finite satisfiabilty method adds to the Lenzerini and
Nobili method an O(n) time complexity, where n is
the size of the class diagram (including associations,
classes and class hierarchy constraints).
43
Finite Satisfiabilty over Unconstrained Tree Hierarchy
Proof [Correctness Claim]
CD: finitely satisfiable
A class diagram
that includes binary
associations and
unconstrained tree
hierarchy
CD’: finitely satisfiable
Class Diagram
Create the Lenzerini
without hierarchy
& Nobili inequalities
constraint
system and Solve.
It is sufficient to show a reduction of the finite satisfiability
problem for CD to finite satisfiability problem
for CD’ without generalization sets.
44
Finite Satisfiabilty over
Unconstrained Tree
Hierarchy
Reduction Proof
CD: finitely satisfiable
I
CD
CD’
Lenzerini & Nobili
inequalities
CD’: finitely satisfiable
I’
45
Consistency notions (1)
•
Berardi et al (2005), distinguish two cases:
– Consistency of class diagram – has an instantiation
with at-least one non-empty class extension.
– Class consistency – there is an instantiation in
which the class extension is non-empty.
The whole class diagram is
consistent
Consistent
rest of the diagram
46
Consistency notions (2)
• All class consistency of a class diagram –
every class is consistent.
• Full consistency of a class diagram – has
an instance in which all class extensions are
non-empty.
47
Finite satisfiability notions
• All class finite satisfiability of a class diagram – every
class there is a finite instance in which the class
extension is non-empty (strong satisfiability, Lenzerini
and Nobili, 1990).
Research Contribution
Lenzerini & Nobili 92
UML Class Diagram
• Finite satisfiability of a class diagram – it has a finite
instance in which all class extensions are non-empty.
48
Class Diagram: Cardinality
Constraint and Class Hierarchy
Advisor
Employment
1..*
+employee
1
University
+employer
• Class: Advisor and University
Master
PhD
• Association: Employment
– Cardinality Constraint
Legal Instance:
mari : Advisor
• Class Hierarchy
employment
+employee
employment
rami : Advisor
Master
+employee
+employer
+employer
BGU : University
49
Class Diagram: Generalization Set
Concept
Female
Advisor
Employment
1..*
+employee
1
University
+employer
Male
{overlapping,incomplete}
{disjoint,
complete}
{overlapping,
{disjoint,
incomplete}
complete}
Master
jame
jame ::Advisor
Master
PhD
marirami
: Master,
PhD
: Master
employment
+employee
+employer
BGU : University
50