Development of a complex system relies on di erent yet related models each representing the system from a particular perspective. In this respect, an important task is to check consistency between related models to guide subsequent decisions concerning consistency restoration. Triple Graph Grammars (TGGs), a particular dialect of graph grammars, are well-suited for describing consistency of two models together with correspondences. The grammar-based description leads to a precise consistency notion which is prerequisite for reliable consistency checks, and correspondences serve as explicit traceability information. Consistency checks with TGGs, however, turn out to be more di cult than consistency restoration in most cases and have not been addressed su ciently so far. We rst discuss why consistency checks with TGGs are worthwhile and identify backtracking issues making correct and e cient consistency checks challenging. Finally, we present two strategies to overcome these challenges, re ecting our work in progress towards a formally-founded consistency check approach with viable tool support.
is to nd a valid MC if there exists one. In case of inconsistency, a partial triple MS M S0 M C0 ! M T0 MT must be explored to indicate which parts of MS and MT correspond to each other and which parts do not. Related work. QVT-R [OMG15] is currently the only available standard for consistency checks. The main idea here is to specify a set of relations that must hold between MS and MT . The standard [OMG15] de nes the semantics of QVT-R by translating it to QVT Core. The major problem, however, is that no su cient formalization is provided for QVT-R and its translation to QVT Core. Consequently, scarce tool support can be observed and seminal contributions to QVT-R address de ning clear semantics in the rst place: In [Ste09], consistency checks with QVT-R are formalized as a game between a veri er and a refuter whose interest is to satisfy or to contradict relations, respectively. In [GdL12], QVT-R is translated to graph constraints which resort to similar formal techniques as TGGs (but without correspondences). In [MC13], QVT-R is translated to predicates over models and a solver is employed for consistency checks. Considering these state-of-the-art QVT-R approaches, the following three arguments motivate us to establish consistency checks with TGGs: - Grammar-based consistency has a clear semantics (a model pair can either be constructed by the grammar or it cannot). Thus, given MS , MT , and a TGG, the consistency check is precisely and fully de ned without having to translate the TGG to another formalism as done for QVT-R. Finding the correct answer e ciently is the only obstacle between theory and tool support where all TGG tools can share a common formal foundation. - In QVT-R, consistency must be understood and checked separately in two directions. A direction-agnostic consistency notion as in TGGs, however, is arguably easier to manage for both bx tool developers and users. - Correspondences in TGGs can be used for traceability purposes (e.g., change impact analysis). A partial correspondence model between inconsistent models, moreover, indicates the extent of consistency violation. QVT-R formalizations do not support traceability (with the exception of a trace-based but restrictive game variant in [Ste09]) whereas [OMG15] uses implicit traces in the underlying QVT Core translation. As argued again in [Ste09], however, these traces do not capture both directions as they are created in two directions separately. The pioneer work concerning consistency checks with TGGs is [EEH08] where operational grammar rules that create correspondences for two given models are derived from a TGG. How to apply these rules in a correct order, however, remains an open issue and, if done naively, requires backtracking in many cases as we shall point out in Section 2. In [HEO+15, EEGH15], furthermore, these operational grammar rules are extended such that existing correspondences between two models are examined and only missing ones are created (backtracking is still required for missing correspondences). In this regard, backtracking issues can actually be mitigated when consistency checks (and correspondence creations) are performed frequently after every small modi cation on models and exiting correspondences are used in each run to reduce backtracking points. However, consistency checks between two large models that do not have any correspondences in between (as they are not necessarily maintained in a TGG-based environment from the beginning) are not su ciently addressed. We focus on this case as consistency checks are typically not considered and performed in every intermediate step of a development process but rather after models have reached an advanced state.
Arguably due to backtracking issues, TGG tools generally do not support consistency checks. The only exception is HenshinTGG1 whose consistency checks, however, only work if no decision point to be backtracked exists and fail otherwise as is already the case for simple TGGs we have experimented with. To improve the situation, we present in Section 3 two viable strategies towards providing fully- edged tool support. 2
Background, Example, and Wrong Choices of Correspondences Our example2 deals with the consistency between UML operations with parameters and their Java counterparts. The left part of Figure 1 shows a consistent model pair (ignore the correspondences in the middle for now). The UML model as well as the Java model represent two operations, both named substring. Both operations have a parameter beginIndex whereas one of the operations has an additional parameter length. In general, consistent models in our example are simply isomorphic (this already su ces to reveal the complexity of consistency checks).
The right part of Figure 1 shows two TGG rules to create UML and Java models with correspondences in between, constituting thus a grammar for consistent triples of models. TGG rules are monotonic, i.e., they only create elements and never delete. Created elements in a rule are depicted green with a ++-markup where black elements represent the context required to apply the rule. The rst rule (OperationRule) creates a pair of UML and Java operations with equal names and a correspondence in between. Similarly, the second rule (ParameterRule) creates a pair of UML and Java parameters for an existing pair of operations.
1http://github.com/de-tu-berlin-tfs/Henshin-Editor/wiki/Manual-for-HenshinTGG-Editor 2Available in the bx example repository at http://bx-community.wikidot.com/examples:umloperationstojavaoperations u1 : UMLOperation name=“substring“ u2 : UMLParameter name=“beginIndex“ u3 : UMLOperation name=“substring“ u4 : UMLParameter name=“beginIndex“ u5 : UMLParameter name=“length“ u1j1 u2j2 u3j3 u4j4 u5j5 j1 : JavaOperation name=“substring“ j2 : JavaParameter name=“beginIndex“ j3 : JavaOperation name=“substring“ j4 : JavaParameter name=“beginIndex“ j5 : JavaParameter name=“length“
uo :
UMLOperation ParameterRule: ++
uo : UMLOperation
++ up : UMLParameter uo.name == jo.name ++ uojo uojo ++ upjp up.name == jp.name
++ jo : JavaOperation
jo : JavaOperation
++ jp : JavaParameter ++
While TGG rules create models simultaneously, operataailtolenmmaloisdrsueinllsegsboaunrteesmaduaetrpokemn(aid.teiin.c,galpolyrnodcteehsresiv)oepedxeriwsathtiiinocgnhaodlnosecsneonatanrcdiroe.carItene- ☐U→ML☑Opueora:tion uo++jo ☐J→av☑aOjpoer:ation a forward transformation, for example, an existing source uo.name == jo.name model is marked while a correspondence and a target model are created (backward analogously). In a consistency check, ParameterRule_ConsistencyCheck: an existing source and target model are marked pairwise ☑ ☑ sauncdceaedcsorirfesbpootnhdmenocdeemls oadreel mis acrrkeeadtecdo.mCpolentseilsyt.enFcyigcuhreeck2 UMLOpueora:tion uojo JavaOjpoer:ation depicts the consistency check rules derived for our TGG caoccnosrisdtienngcytochtehcek rfourlemsaplirzaacttiiocnalliyn s[iEmEuHla0te8]c.reaMtiaornksiningsthine ☐U→ML☑Paurpam:eter up+j+p ☐J→av☑aPjapra:meter original TGG rules (depicted as 2 ! 2 which simply replaces the ++-markup). Applying these rules, the corre- up.name == jp.name spondences shown to the left of Figure 1 can be created and Figure 2: Consistency check rules the model pair is then identi ed to be consistent. As shown in [EEH08], moreover, an application sequence of consistency check rules always exists to mark consistent models completely. How to nd this sequence, however, remains an open issue and turns out to be challenging. nua1me:=“UsMuLbOspterriantgi“oningInthFeigcuornues1ij3s1,teanncyuncdhee☑scinkjra1emrde:u=“lJoesausuvtbacsOintporemirFnaegti“giooufnreap2pltyo- ☑nua1me:=“UsMuLbOspterriantgi“on u1j3 ☑nja1me:=“JsauvbasOtpreirnagt“ion our model pair is depic☑ted. Consistency check ☑ ☑ nua2me:=“UbMeLgPianrIanmdeetxe“rfaalliyls cionntshisitsue2ncjat2.seTahltehopurogbhnjal2emtme:h=e“JbaismevgatioPhnadIraenatldmseeixtna“edrreivaidcutua-l nua2me:=“UbMeLgPianrIanmdeetxe“r u2j4 nja2me:=“JbaevgaiPnaIrnadmeext“er consistency check rules ☑can connect wrong pairs ☑ ☑ nua3me:=“UsMuLbOspterriantgi“onof model elue3mj3ents. For enja3xmae:m=“JpsauvlbaesO,tpreairnawgt“iroonng pair nua3me:=“UsMuLbOspterriantgi“on u3j1 nja3me:=“JsauvbasOtpreirnagt“ion of substring operations is connected in Fig
☑ ☑ ☑ nua4me:=“UbMeLgPianrIanmdeetxe“rounre b3o. tAhssaiduce4ojs4nrseemquaeinncue,nnjmta4hmaee:r=lk“JeebaedvngagiPwntaIrhinatdmhpeeoaxtu“erratmcoetrerers- nua4me:=“UbMeLgPianrIanmdeetxe“r u4j2 nja4me:=“JbaevgaiPnaIrnadmeext“er spondence (as their par☑ents are mistakenly not ☐ ☐ u5 : UMLParameterconnected).u5jO5bviously, cjo5ns:isJtaevnaPcayracmheteecrks with u5 : UMLParameter j5 : JavaParameter name=“length“ TGGs require backtrackinnagmei=n“legnegnteh“ral if no ap- name=“length“ name=“length“ propriate control mechanism is used to govern Figure 3: Undesired consistency check result correspondence choices. Interestingly, most of the wrong decisions are not relevant for forward (or backward) transformations but only for consistency checks. That is, pairwise marking of model elements introduces new decision points other than those in one-sided marking and leads a consistency check easily to an incorrect result.
Strategies for Reliable and Scalable Consistency Checks We do not consider backtracking to be a satisfactory solution. Firstly, backtracking may repeatedly discard and produce the same correspondences until a wrong decision in an arbitrary depth is corrected. Secondly, and more critically, inconsistent models directly lead to exhaustive backtracking without success whereas one of the discarded attempts may actually be of interest for a partial correspondence model. We instead discuss two strategies for reliable and scalable consistency checks without backtracking.
Create all then lter. A viable strategy ☑ ☑ ☑ ☑ caograrienssptonbdaeckntcreasck(iinncgluidsintgo ucnrdeaestiereadllonpeoss)sibbele- nua1me:=“UsMuLbOspterriantgi“on uu11jj13 nja1me:=“JsauvbasOtpreirnagt“ion tween two models in a brute-force manner and ☑u☑2 : UMLParameter u2j2 ☑j☑2 : JavaParameter to determine a correct subset automatically in name=“beginIndex“ u2j4 name=“beginIndex“ reeletmroesnptescta.reIncothnissidcearseed, stoombeesomuarrckeeadnmdutaltrigpelet ☑u☑3 : UMLOperation u3j1 ☑j☑3 : JavaOperation times as demonstrated in Figure 4 for our exam- name=“substring“ u3j3 name=“substring“ ple. A subset of correspondences must be then ☑u☑4 : UMLParameter u4j2 ☑j☑4 : JavaParameter determined such that each element is marked ex- name=“beginIndex“ u4j4 name=“beginIndex“ actly once for consistent models or at most once ☑ ☑ fcoiersinbceotnwseiestnencotrmreospdoelnsd.eFnocertsucnaantebley,udseepdefnodreann- nua5me:=“UlMeLnPgatrha“meter u5j5 nja5me:=“JlaevnagPtahr“ameter automated decision: Some correspondences are Figure 4: All possible correspondences essential as they are the only ones marking their connected elements, e.g., u5j5 in Figure 4. Some correspondences imply others, e.g., u5j5 implies u3j3 as it can only be created under u3j3. Finally, some correspondences are mutually exclusive alternatives, e.g., u3j3 and u3j1 as they both mark u3. A Boolean formula consisting of three parts can describe these dependencies as follows () denotes implication and denotes xor ): Essentials: u5j5 Implications: (u2j2 ) u1j1) ^ (u4j4 ) u3j3) ^ (u5j5 ) u3j3) ^ (u2j4 ) u1j3) ^ (u4j2 ) u3j1) Alternatives: (u1j1 u1j3) ^ (u1j1 u3j1) ^ (u2j2 u2j4) ^ (u2j2 u4j2) ^ (u3j3 u3j1) ^ (u3j3 u1j3) ^ (u4j4 u4j2) ^ (u4j4 u2j4)
Choosing the essential correspondence u5j5, from implications follows that u3j3 must also be in the set of chosen correspondences. Consequently, u3j1 and u1j3 (alternatives of u3j3) as well as their implying correspondences u2j4 and u4j2 are excluded. From further implications and alternatives follows that u1j1, u2j2, and u4j4 must be chosen as well. In general, the satisfaction of such a formula can either be outsourced to a solver or it can be implemented with a hand-crafted procedure optimized for the speci c purpose of correspondence analysis. Two main advantages against backtracking are: (i) all (wrong and correct) correspondences are created only once in a progressive search and not repeatedly, and (ii) a partial correspondence model in case of inconsistency is not discarded and can be determined from all possible correspondences in the same manner. Nevertheless, the scalability of this strategy (in terms of runtime and memory consumption) strictly depends on the number of alternative correspondences. Scalable consistency checks can be expected when alternative correspondences only occur locally between two models and not in a combinatorial manner between all elements. Heuristic-based or case-speci c look-ahead. When the number of alternative correspondences grows rapidly, it is more advantageous to make decisions among correspondences already at rule application time (and not in retrospect after all possible correspondences are created). Collecting a set C of possible correspondence candidates that would mark a particular model element e, a consistency check procedure must provide and utilize a function choose(C,e) = c that takes C and e as input, looks ahead for upcoming elements, and returns the best correspondence c 2 C. Beginning with the UML operation u1 in our exemplary model pair, choose(fu1j1, u1j3g,u1) = u1j1 already leads the consistency check procedure to a correct sequence of later correspondence creations, i.e., no other undesired correspondence occurs in the process after connecting the rst UML operation to its correct counterpart in the Java model. In general, when choosing a correspondence connecting two elements, the underlying look-ahead mechanism can be supported by heuristics such as the conformance of (transitive) child elements on both sides, ideally grouped according to any relevant type and attribute information. Case-speci c behaviour of choose, nevertheless, must be allowed by a TGG tool that supports consistency checks and implemented by the TGG designer who should be aware of the discussed backtracking issues. An interactive implementation of choose where the ultimate user (who executes a consistency check) is confronted with these choices should only be considered if there is no feasible automatic decision. 4
Conclusion and Future Work Two particular strategies are presented to avoid backtracking in consistency checks: one brute-force strategy with automated decisions and one look-ahead strategy relying on heuristics or case-speci c expertise. It is also worthwhile to consider a combination of both, i.e., eliminating some alternative correspondences via a lookahead and creating all others for an automated decision. Our next goal is to experiment with these strategies and to come up with tool support which will then be evaluated in industrial consistency tasks. Finally, it is also worthwhile to integrate these strategies into cases where consistency checks start with existing correspondences by utilizing further operational rules of [HEO+15, EEGH15].
Acknowledgement This work has been funded by the German Federal Ministry of Education and Research within the Software Campus project GraTraM at TU Darmstadt, funding code 01IS12054. [EEH08]
Hartmut Ehrig, Karsten Ehrig, and Frank Hermann. From Model Transformation to Model Integration based on the Algebraic Approach to Triple Graph Grammars. ECEASST, 10, 2008. [MC13]
Nuno Macedo and Alcino Cunha. Implementing QVT-R Bidirectional Model Transformations using Alloy. In Vittorio Cortelessa and Daniel Varro, editors, FASE 2013, volume 7793 of LNCS, pages 297{311. Springer, 2013. [OMG15] OMG. QVT Speci cation, V1.2, 2015.
Andy Schurr. Speci cation of Graph Translators with Triple Graph Grammars. In Ernst W. Mayr, Gunther Schmidt, and Gottfried Tinhofer, editors, WG 1994, volume 903 of LNCS, pages 151{163. Springer, 1994.