Report

Logic Programming Based Model Transformations An overview of related work GOAL – WHY? • Exploring the reasoning techniques for querying the inconsistencies in Models and model transformations • State of the art, challenges, gaps and how we can contribute • Simplify transformations between ISO and CCOM Logic programming language Answer Set Programming (ASP) Declarative Search problems to find stable models answer set solvers — programs for generating stable models—are used to perform search Alloy lightweight formal specification language declarative based on first-order logic based on relational logic > effective to validate and verify object-oriented models automatic model finding via SAT solving Alloy model consists of Signatures, Relations, Facts and Predicates. Alloy Analyzer (Simulation & Assertion) Prolog first-order logic relations represents facts and rules. A computation is initiated by running a query over these relations RELATED WORK Antonio Cicchetti, Davide Ruscio, Romina Eramo, and Alfonso Pierantonio. JTL: A Bidirectional and Change Propagating Transformation Language. In SLE 2011, volume LNCS 6563, pages 183-202. Springer, 2011. Johannes Schoenboeck, Angelika Kusel, Juergen Etzlstorfer, Elisabeth Kapsammer, Wieland Schwinger, Manuel Wimmer, and Martin Wischenbart. CARE - A Constraint-Based Approach for Re-Establishing Conformance Relationships. In APCCM 2014, CRPIT Vol.154, pages 19-28. ACS, 2014 Anastasakis, K., Bordbar, B., & Küster, J. M. (2007, October). Analysis of model transformations via Alloy. In Proceedings of the 4th MoDeVVa workshop Model-Driven Engineering, Verification and Validation (pp. 47-56). Nuno Macedo and Alcino Cunha. Implementing QVT-R bidirectional model transformations using Alloy. In Fundamental Approaches to Software Engineering, pages 297-311. Springer, 2013. Zoltan Balogh and Daniel Varro. Model transformation by example using inductive logic programming. SoSyM, 8(3):347-364, 2009. JesusM. Almendros-Jimenez and Luis Iribarne. A model transformation language based on logic programming. In SOFSEM 2013, volume LNCS 7741, pages 382-394. Springer, 2013. CARE approach(ASP) • Each metamodel elements > class, attribute and reference ASP facts. • Model elements > object, value and link ASP facts. • Conformance constrains have been manually defined [in pseudocode in table] and encoded in ASP. • Meta-model specific Ecore/OCL constrains > ASP constrains in future version of prototype. • Language semantics(object-oriented) need to be encoded as well. • Ecore <> ASP transformations are implemented by Xtend (a flexible and expressive dialect of Java) • A constraint solver produces an output, which is a set of facts describing which objects, values, and links are conform or not, and adds these new facts to the CARE knowledge base. JTL approach(ASP) • Modeled as Graphs composed of nodes, edges and properties – logic assertions • (1)Each (meta)model elements > metanode, metaedge, and metaprop predicate symbols • (1)Each model element > node, edge, property • (2)JTL(QVT-R like syntax) > ASP relation and constrains by means of ATL transformation • (4)Transformation (JTL) engine is based on ASP bidirectional transformation program executed by DLV solver(find stable models) Transformation process steps: 1. the execution engine induces all the possible solution candidates according to the specified relations; 2. the set of candidates is refined by means of constraints (ASP rules). (3)Target model is deducted based on ASP rules from candidate solutions. Analysis of MT(Alloy) • based on meta-modelling • MOF meta-models/OCL > Alloy by means of UML2Alloy transformation tool • Transformation rules > Alloy mapping relation • STEPS Step 1:Translate the Model Transformation Specification to Alloy. Step 2: Analysis using the Alloy Analyzer. • Alloy model of MT which can be analysed by Analyzer(Simulation) QVT-R Bidirectional (Alloy) • UML(annotated with OCL) + QVT-R > Alloy • principle of least change restores consistency by simply returning target models that are at a minimal distance from the original -> the“checkbefore-enforce” policy (QVT-R) is satisfied. • Classes and associations (including attributes) > signatures and relations in Alloy. Inheritance relationship in Alloy. • For each relation R > Alloy predicates to specify Rforward and Rbackward • Predicates are used to specify the when and where clauses, and the domain patterns of each relation • checkonly mode - check the consistency predicate for a pair of models PTL approach(Prolog) • Each (meta) model elements > set of classes, attributes, roles and helpers. • Each model elements > set of classes, attributes, roles, helpers and objects. • PTL > Prolog encoding - based on a Prolog library for handling metamodels • PTL (ATL like syntax) = ATL style rules + logic Rules in Prolog(helpers). Prolog style rules serve as a query language. Prolog is used as a transformation engine for PTL. • A Prolog program is automatically obtained from a PTL program. The encoding of PTL programs with Prolog is based on a Prolog library for handling meta-models Inductive logic(Prolog) • Modeled as Graphs composed of nodes, edges and properties – logic assertions • Source and target models are mapped into Prolog clauses • Mapping models are represented by tuples ref (ri , src1, . . . , srcn, trg1, . . . , trgm). Conclusions • Logic clause, fact, assertion = represents models and meta-models • Logic rule = used to encode model transformation and constraints on models • taking advantage of model finding(SAT-solver) abilities • Being solver-based, the main drawback is performance - incremental solving techniques - mechanisms to infer which parts of target model can be fixed in design time • Model & transformation > logic programming is manual, except in JTL approach