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 bcd 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 ecd 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