DocumentCode :
1812642
Title :
Efficient recognition of finite satisfiability in UML class diagrams: Strengthening by propagation of disjoint constraints
Author :
Maraee, Azzam ; Balaban, Mira
Author_Institution :
Ben-Gurion Univ. of the Negev, Beer-Sheva
fYear :
2009
fDate :
2-5 March 2009
Firstpage :
1
Lastpage :
8
Abstract :
Models lie at the heart of the emerging Model-driven Engineering approach. In order to guarantee precise, consistent and correct models, there is an urgent need for efficient reasoning methods for verifying model correctness. This paper extends and strengthens our previous work on efficient recognition of finite satisfiability problems in UML class diagrams with constrained generalization sets. First, algorithm FiniteSat is simplified into a single stage process, yielding a more compact linear inequality system. The main contribution of the paper is a method for propagation of disjoint constraints within complex class hierarchy structures, which meaningfully extends the scope of the FiniteSat algorithm. The method relies on a thorough analysis of the interaction between disjoint constraints and the structure of class hierarchy. It is recommended as a pre-processing stage, and being an anytime algorithm, even partial application is useful.
Keywords :
Unified Modeling Language; computability; program verification; reasoning about programs; FiniteSat algorithm; UML class diagram; complex class hierarchy structure; disjoint constraint propagation; finite satisfiability recognition; linear inequality system; model correctness verification; model-driven engineering; reasoning method; Unified modeling language;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Model-Based Systems Engineering, 2009. MBSE '09. International Conference on
Conference_Location :
Haifa
Print_ISBN :
978-1-4244-2967-7
Electronic_ISBN :
978-1-4244-2968-4
Type :
conf
DOI :
10.1109/MBSE.2009.5031714
Filename :
5031714
Link To Document :
بازگشت