Advanced Techniques and Tools for Secure Collaborative Modeling Csaba Debreceni Budapest University of Technologies and Economics, Department of Measurement and Information Systems MTA-BME Lendület Research Group on Cyber-Physical Systems Email: {debreceni}@mit.bme.hu Abstract—Model-based systems engineering of critical cyber- exist to support such scenarios, additional challenges arise physical systems necessitates effective collaboration between dif- that cannot be naturally extended from traditional code-based ferent collaborators, teams, stakeholders. Engineering artifacts approaches due to the graph-like nature of the artifacts. stored in model repositories are concurrently developed in either offline (checkout-modify-commit) or online (GoogleDoc-style) scenario where the confidentiality and integrity of design artifacts A. Secure Collaborative Modeling need to be protected by access control policies. Unfortunately, tra- ditional approaches for managing concurrent code development An increased level of collaboration in a model-driven de- do not naturally extend to collaborative modeling which implies velopment process introduces additional confidentiality chal- novel challenges. lenges to sufficiently protect the intellectual property of the My research focuses on developing (i) a general secure col- laboration scheme that guarantees that high-level access control collaborating parties, which are either overlooked or signif- policies are respected during collaboration and it can be inte- icantly underestimated by existing initiatives. Even within a grated into existing version control systems (e.g. SVN) to support single company, there are teams with differentiated responsi- offline scenario; (ii) automated merging and fine-grained locking bilities, areas of competence and clearances described by high- to enhance the efficiency of conflict resolution and prevention level access control policies. Such processes likewise demand upon concurrent modification of the models; (iii) derivation and incremental maintenance of view models to provide specific focus confidentiality and integrity of certain modeling artifacts. of the designers by abstracting from unnecessary details of the Existing practices for managing access control of models underlying system model. rely primarily upon the access control features of the back- end repository. Coarse-grained access control policies aim to I. P ROBLEM AND M OTIVATION restrict access to the files that store models. For instance, EMF The adoption of model driven engineering (MDE) by system models can be persisted as standard XMI documents, which integrators (like airframers or car manufacturers) has been can be stored in repositories providing file-based access and steadily increasing in the recent years [1], since it enables to change management (as in SVN [4], CVS [5]). Fine-grained detect design flaws early and generate various artifacts (source access control policies, on the other hand, may restrict access code, documentation, configuration tables, etc.) automatically to the model on the row level (as in relational databases) or from high-quality system models. triple level (as in RDF repositories). Unfortunately, coarse- The use of models also strengthens collaboration between grained security policies are captured directly on the storage distributed teams of different stakeholders (system integra- (file) level often result in inflexible fragmentation of models tors, software engineers of component providers/suppliers, in collaborative scenarios. hardware engineers, certification authorities, etc.) via model As a result, coarse-grained access control can lead to repositories, which significantly enhances productivity and significant model fragmentation, which greatly increases the reduces time to market. An emerging industrial practice of complexity of storage and access control management. In system integrators is to outsource the development of various industrial practice, automotive models may be split into more design artifacts to subcontractors in an architecture-driven than 1000 fragments, which poses a significant challenge for supply chain. tool developers. Some model persistence technologies (such as Collaboration scenarios include traditional offline collab- EMFs default XMI serialization) do not allow model fragments orations with asynchronous long transactions (i.e. to check to cyclically refer to each other, putting a stricter limit to out an artifact from a version control system and commit fragmentation. Hence, MDE use cases often demand the ability local changes afterwards) as well as online collaborations to define access for each object (or even each property of each with short and synchronous transactions (e.g. when a group object) independently. of collaborators simultaneously edit a model). Even though, Furthermore, coarse-grained access control lacks flexibil- various collaborative modeling frameworks (like [2], [3], etc.) ity, especially when accessing models from heterogeneous information sources in different collaboration scenarios. For This paper is partially supported by the EU Commission with project MONDO (FP7-ICT-2013-10), no. 611125. and the MTA-BME Lendület 2015 instance, they disallow type-specific access control, i.e., to Research Group on Cyber-Physical Systems. grant or restrict access to model elements of a specific type (e.g., to all classes in a UML model), which are stored in II. P RELIMINARIES multiple files. A. Related Work My first research question is constructed as follows: 1) Secure Collaborative Modeling: Traditional version con- RQ-1 How to capture and enforce high-level access control trol systems (like [4]) adopt file-level access policies, which policies during collaborative modeling? are clearly insufficient for fine-grained access control speci- fications. [2] allows for role-based access control with type- B. Conflict Prevention and Resolution specific (class, package and resource-level) permissions, but Enabling a high degree of concurrent edits for collabora- disallows instance level access control policy specifications. tors is required to make the traditionally rigid development Access control is not considered in recent collaborative mod- processes more agile. The increasing number of collaborators eling environments like [8], [9], [10], [3], [11], [12], or the concurrently developing artifacts increases the probability of tools developed according to [13]. [14] provides fine-grained introducing conflicts. Conflict avoidance techniques such as role-based access control for online collaboration but no offline locks try to prevent conflicts by letting the users request that scenario is supported, though. Both online collaboration and certain engineering artifacts should be made unmodified by role-based access control with type-specific (class, package all other participants for a duration of time. But it usually and resource-level) permissions is provided in [2], but no leads to unnecessary preventions (locks) which significantly facility for instance level access control policy specifications. limits the degree of concurrent development and does not scale However, there is a pluggable access control mechanism that with the increasing number of collaborating teams. Model can specify access on the object level. merging aims to resolve the conflicts, but, it can be complex 2) Locking Support: The state-of-the-art locking techniques tasks as the interdependence within a model makes conflicts are the fragment-based and object-based locks. Fragment- easy to introduce and hard to resolve. Furthermore, domain- based locking requires that models are partitioned into storage specific conflict resolution strategies are rarely taken into fragments, e.g. files or projects and entire fragments can be consideration in industrial frameworks (e.g. EMF Compare[6], locked at once. Object-based locking locks individual model EMF Diff/Merge[7]), hence the well-formedness of merge objects (including their attributes and connections) which results is questionable. requires to inspect the structure of the model. My second research question is the following. Existing collaborative modeling tools either lack locking support or implement rigid strategies such as fragment-based RQ-2 How to provide fine-grained prevention and automa- locking, or locking subtrees or elements of a specific type, tized resolution strategies of conflicts? which hinder effective collaboration. Most of offline collabo- rative modeling tools [5], [15], [3], rely on traditional version C. Bidirectional Synchronization of View Models control systems using file-based (same as fragment-based) locking with contributors committing large deltas of work. Views are key concepts of domain-specific modeling in Model repositories [2], [9], support both implicit and explicit order to provide task-specific focus (e.g., power or com- locking of subtrees and sets of elements. These locks can munication architecture of a system) to engineers by creating prevent others from modifying elements to avoid conflicts. On- a model which highlights only some relevant aspects of the line collaborative modelling frameworks [11], [8], [10], [14], system to help detect conceptual flaws. Typically multiple rely on a short transaction model: a single, shared instance of view models are defined for a given an underlying source the model is concurrently edited by multiple users, with all model, which need to be refreshed automatically (or upon user changes propagated to all participants instantaneously. These request) upon changes in the source model. approaches use timestamped operations to resolve conflicts or Usually, these views are represented as models themselves provide only lightweight lock mechanisms, e.g., explicit locks (view models), computed from the source model. On one to certain elements. hand, the efficient forward propagation of changes from the 3) Conflict Resolution in Model Artifacts: Model compar- source model to the views is challenging, as recalculating the ison refers to identifying the differences between models. view from scratch has to be avoided to achieve scalability. Based on its result, model merge synthesizes a combined On the other hand, the efficient backward propagation of model which reconciles the identified differences. My research complex changes from one or more abstract view models to focuses on three-way merge, which uses the common ancestor the underlying source model resulting in valid and well-formed O of local copy L and remote copy R to derive the merged models is also a challenging task which requires to limit the model M . To determine the changes executed on O, a compar- propagation to a well-defined part of the source model to ison is conducted between O ↔ L and O ↔ R. The solution achieve scalability. of merge M is obtained by applying a combination of changes My third research question is as follows. performed either on L or R to the original model O. RQ-3 How to derive and incrementally maintain view Most approaches [6], [7], [16], [17], [18] are semi- models and trace back complex changes to the underlying automated as they use a two-phase process: (i) first, they source models? apply the non-conflicting operations and then (ii) let the user prioritize and select the operation to apply in case of two conflicting changes. This always results in a single solution due to the manual resolution by the user. In comparison, [19], [20] resolve the conflicts automatically in different ways and offer several solutions. 4) Incremental Maintenance of View Models.: View main- tenance by incremental and live QVT transformations is used in [21] to define views from runtime models. The proposed algorithm operates in two phase, starting in check-only mode before an enforcement run, but its scalability is demonstrated only on models up to 1000 elements. [8] allows the compo- sition of multiple EMF models into a virtual model based on a composition metamodel, and provides both a model virtualization API and a linking API to manage these models. Fig. 1. MONDO Offline Collaboration - Architecture The approach is also able to add virtual links based on composition rules. In [22], an ATL-based method is presented (gold model) containing all the information and to (ii) prop- for automatically synchronizing source and target models. agate changes introduced into these views back to a server In [23], correspondences between models are handled by in both online and offline scenarios. Access control policies matching rules defined in the Epsilon Comparison Language, consist of rules that allow, obfuscate or deny read and/or but incremental derivation is not discussed. write permissions of model parts identified by graph patterns 5) Backward Propagation: For the backward propagation detailed in [30]. of changes, the use of traceability links is a well-accepted In [31], a collaboration scheme between the clients of approach to define which part of the source model has to multiple collaborators and exactly one server is described to be updated upon a change on the target model. In [24], support fine-grained access control in offline scenario. The these links are stored as a correspondence model where their server stores the gold models and the clients can download maintenance is derived from the TGG rules. [25] also specifies their specific front models. Modifications, executed by a trace classes to facilitate and maintain traceability links. [26] clients, are submitted to the server and they are accepted if stores traceability links in Alloy[27] as a bijective mapping. write permissions are successfully checked. Right after the [28] uses a weaving model that stores the traces of references submission, the changes are propagated to the other front between different models in the view, however all objects in model while read permissions are enforced. Finally, clients the view model act as proxies to an object in the source model. can downloaded their updated front models. The scheme is realized by extending SVN[4] using its hooks. B. Foundational Techniques The server and clients are realized as a gold repository and 1) Graph Patterns: A graph pattern represents structural multiple front repositories, respecively. The gold repository constraints prescribing the interconnection between nodes and contains gold models, but it is not accessible to collaborators. edges of given types extended with algebraic expressions to Each collaborator is assigned to a specific front repository define attribute constraints. Pattern parameters are a subset containing a full version history of the front models. Change of nodes and attributes representing the model elements in- propagations are maintained between the repositories. As a teresting from the perspective of the pattern user. A match of result, each collaborator continues to work with a dedicated a pattern is a tuple of pattern parameters that has the same VCS as before, thus they are unaware that this front repository structure as the pattern and satisfies all structural and attribute may contain filtered and obfuscated information. constraints. My contributions related to the fulfillment of RQ-1 : 2) Design Space Exploration: Design space exploration (DSE) aims to find optimal design candidates of a domain Contribution 1 I proposed a generic modeling language to with respect to different objectives where design candidates are capture fine-grained access control policies integrated into a constrained by complex structural and numerical restrictions provenly secure collaborative architecture. (e.g. described by graph pattern) and are reachable from an C1.1 Access Control Language. I proposed a rule-based initial model by applying a sequence of exploration rules. access control language to describe high-level and fine- grained policies in both online and offline scenarios. Rules III. OVERVIEW OF THE A PPROACHES may allow, obfuscate or deny read and/or write permissions A. General Secure Collaboration Scheme of model parts identified by graph patterns[30], [31]. C1.2 Read and Write Dependencies. I analyzed read and Approach. In [29], we proposed a query-based approach for write dependencies implied by high-level access control modeling fine-grained access control policies, and we defined policies as read and write permissions of a model part bidirectional model transformations to (i) derive filtered views (front models) for each collaborator from the original model may depend on other model parts implied by internal consistency rules [30]. C1.3 Formalization of Transformation Rules. I formalized transformation rules to derive secure front models with respect to the read and write permissions [31]. C1.4 Secure Collaboration Scheme. I formalized a collab- oration scheme as communicating sequential processes (CSP) to enforce high-level access control policies. I spec- ified correctness criteria and proved the correctness of the scheme [31]. C1.5 Realization of Secure Collaboration. I realized the col- laboration scheme in case of offline scenarios by extending an existing version control system to enforce fine-grained access control while collaborators can use off-the-shelf tools [32], [31]. Fig. 2. Behavior of Property-Based Locks C1.6 Evaluation. I evaluated the scalability of the collabo- ration architecture on a case study of offshore wind turbine controllers [29], [32], [33], [31]. The bidirectional transformation and the algorithm to derive effective permission based on the proposed language is the contribution of Gábor Bergmann whereas the concept of the common architecture to support both online and offline scenarios is the contribution of István Ráth. Uniqueness. Our provenly correct collaboration scheme is able to enforce fine-grained access control policies of modeling artifacts over existing version control system in case of offline scenarios. The scheme and its realization is Fig. 3. Architecture of DSE Merge demonstrated in [32] as an integration with SVN[4]. B. Conflict Reduction and Handling (i) the well-formed merged model M ; (ii) the set of non- executed changes ∆L0 ,∆R0 ; and (iii) the collection of the Approach. In our preliminary work [34], we introduced the deleted objects stored in Cemetery. concept of property-based locking where collaborators request My contributions related to the fulfillment of RQ-2 : locks specified as a property of the model which need to be maintained as long as the lock is active. Hence, other Contribution 2 I proposed a fine-grained property-based collaborators are permitted to carry out any modifications that locking technique to avoid conflicts and an automated three- do not violate the defined property of the lock. In [35], the way model merge technique to resolve conflicts. realization of property-based locking strategy is proposed as a C2.1 Fine-grained Property-based Locking. I proposed a common generalization of existing fragment-based and object- property-based locking technique as generalization of tradi- based locking approaches. Complex properties are described as tional fragment-based and object-based locking techniques graph patterns to express structural (and attribute) constraints which captures fine-grained locks as graph patterns and for a model where the result set, i.e. the matches of graph pat- exploits incremental query engines to maintain and evaluate tern, can be calculated by pattern matchers or query engines. locks [35]. Only those modifications are allowed that do not change the C2.2 Automated Model Merge using DSE. I proposed an result set of a list of queries as depicted in Fig. 2. automated three way model merge technique by adapting In [36], we proposed DSE-Merge that exploits guided rule- rule-based design space exploration to derive consistent and based design space exploration (DSE) [37] to automate the semantically correct merged models [36], [37]. three-way model merge with an architecture depicted in Fig. 3. C2.3 Realization of DSE-merge. I realized an infrastructure Three-way model merge is applied to DSE problem where of automated model merge over EMF integrated into the the initial model consists of the original model O and two Eclipse IDE [36], [32]. difference models (∆L and ∆R); the goal is that there are C2.4 Evaluation. I evaluated the scalability of the auto- no executable changes left in ∆L and ∆R; operations are mated model merge and I compared the effectiveness of defined by change driven transformation rules to process fine-grained property-based locking and traditional locking generic composite (domain-specific) operators; and constraints strategies for conflict prevention on a case study of offshore may identify inconsistencies and conflicts to eliminate certain wind turbine controllers [36], [35], [33]. trajectories. The output is a set of solutions consisting of Fig. 5. Overview of backward change propagation Fig. 4. Overview of integration architecture Contribution 3 I proposed a novel technique of bidirec- tional synchronization of view models where the forward incremental synchronization is achieved by unidirectional The novel concept of property-based locking has been derivation rules while the backward propagation of changes carried out in a collaborative work [34] where my contribution is generated using logic solvers. is the first adaption in a practical setting. C3.1 Incremental Forward Synchronization. I formalized a Uniqueness. Our property-based approach is general and fully forward incremental, unidirectional synchronization can be used for both implicit locking of subtrees and set technique of view models allowing chaining of views where of elements or explicit locking of a certain element and its the object of view model depend on the match set of the incoming and outgoing references. In addition it extends these precondition of derivation rules [38], [40]. lock types with the definition of properties to provide less C3.2 Change Impact Analysis. I analyzed the impact of restrictive locking for the collaborators. changes in underlying source models in case of backward The closest to our merge approach are [19] and [20], but propagation. The impacted part is added to the logic solver we rely on state-based comparison, apply a guided local- as additional constraints to calculate minimally modified search strategy (vs. [20]), detect conflicts at runtime and allow source model candidates [39]. complex generic merge operations (vs. [19]). Internally, we C3.3 Realization of Forward Synchronization. I realized the uniquely use incremental and change-driven transformations incremental and forward view synchronization technique to derive the merged models. Finally, we reported scalability where elementary derivation rules are captured by graph of merge process for models which are at least one order of patterns and the reactive synchronization process uses the magnitude larger compared to [19] and [20]. Viatra Event-driven Virtual Machine (EVM) [38]. C. Synchronization of View Models C3.4 Evaluation. I evaluated the scalability of the proposed Approach. In [38], we introduced an approach where view approaches on case studies from the avionics and the models are conceptually equivalent to regular models and they health-care domain [38], [39], [40]. are defined using a fully declarative, rule based formalism. Preconditions of rules are defined by graph patterns, which The transformation of the preconditions described by graph identify parts of interest in the source model. Derivation rules patterns and the impacted parts to first order logic is the then use the match set of a graph pattern to define elements contribution of Oszkár Semeráth whereas my contributions of the view model. Informally, when a new match of a query are the impact analysis and the concept of using logic solver appears then the corresponding derivation rule is fired to create for backward propagation extended with impacted parts as elements of the view model. When an existing match of a additional constraints. query disappears, the inverse of the derivation rule is fired to Uniqueness. Definition of a view model is unidirectional, delete the corresponding view model elements. while the forward propagation of the operation-based changes View models derived by a unidirectional transformation are are live, incremental and executed automatically that also read-only representations, and they cannot be changed directly. maintains explicit traces. At backward propagation, using To tackle this problem, we proposed an approach in [39] to partitioning as an additional input of the logic solver improves automatically calculate possible source model candidates for a scalability issues and limits the impact of changes to a well- set of changes in different view models as depicted on Fig. 5. defined part of the source model. First, the possibly impacted partition of the source model is ACKNOWLEDGEMENT need to be identified by observing traceability links to restrict the impact of a view modification. Then the modified view I would like to thank my advisor, Daniel Varro for his models and the query-based view specification are transformed guidance during my research. I would also like to express into logic formulae. Finally, multiple valid resolutions of the my gratitude to Istvan Rath, Gabor Bergmann, Oszkar Se- source model are generated using logic solvers corresponding merath and Akos Horvath as well as Marsha Chechik, Fabiano to the changes of view models and the constraints of the source Dalpiaz, Jennifer Horkoff and Rick Salay along with numerous model from the users can manually select a proper solution. colleagues and co-authors for sharing their ideas. My contributions related to the fulfillment of RQ-3 : R EFERENCES [25] OMG, “MOF 2.0 QVT.” [26] H. Gholizadeh et al., “Analysis of Source-to-Target Model [1] J. Whittle et al., “The State of Practice in Model-Driven Engineering,” Transformations in QueST,” in Proceedings of the 4th Workshop IEEE Software, vol. 31, no. 3, pp. 79–85, 2014. on the Analysis of Model Transformations co-located with (MODELS [2] Eclipse Foundation, “CDO,” http://eclipse.org/cdo. 2015, Ottawa, Canada, 2015, pp. 46–55. [Online]. Available: [3] ——, “EMFStore,” http://eclipse.org/emfstore. http://ceur-ws.org/Vol-1500/paper6.pdf [4] Apache, “Subversion,” https://subversion.apache.org/. [27] D. Jackson, “Alloy Analyzer.” [5] G. Kramler et al., “Towards a Semantic Infrastructure Supporting Model- [28] H. Bruneliere et al., “EMF Views: A View Mechanism for Integrating based Tool Integration,” in GaMMa@ICSE’06. ACM, 2006, pp. 43–46. Heterogeneous Models,” in Conceptual Modeling - ER’15, 2015, pp. [6] Eclipse Foundation, “EMF Compare,” http://eclipse.org/emf/compare/. 317–325. [7] ——, “EMF Diff/Merge,” http://eclipse.org/diffmerge/. [29] G. Bergmann, C. Debreceni, I. Ráth, and D. Varró, “Query-based [8] C. Clasen, F. Jouault, and J. Cabot, “VirtualEMF: A Model Virtualization Access Control for Secure Collaborative Modeling using Bidirectional Tool,” in Advances in Conceptual Modeling. Recent Developments and Transformations,” in MoDELS’16, 2016, pp. 351–361. New Directions, 2011, pp. 332–335. [30] C. Debreceni, G. Bergmann, I. Ráth, and D. Varró, “Deriving Effective [9] J. Tolvanen, “MetaEdit+ for Collaborative Language Engineering and Permissions for Modeling Artifacts from Fine-grained Access Control Language Use (tool demo),” in Tool Demo@SLE’16, 2016, pp. 41–45. Rules,” in COMMitMDE@MoDELS’16, 2016, pp. 17–26. [10] M. Maróti et al., “Next Generation (Meta)Modeling: Web- and Cloud- [31] ——, “Enforcing Fine-grained Access Control for Secure Collaborative based Collaborative Tool Infrastructure,” in MPM@MODELS’14, 2014, Modeling using Bidirectional Transformations,” Software and System pp. 41–60. Modeling, MODELS 2016 Special Section, 2017, submitted. [Online]. [11] Axellience, “Genmymodel.” Available: https://goo.gl/ZAegbo [12] Obeo, “Obeo Designer,” https://obeodesigner.com/en/ [32] C. Debreceni, G. Bergmann, M. Búr, I. Ráth, and D. Varró, “The collaborative-features. MONDO Collaboration Framework: Secure Collaborative Modeling [13] J. Gallardo et al., “A Model-driven Development Method for Collabo- over existing Version Control Systems,” Tool Demo@ESEC/FSE’17, rative Modeling Tools,” J. Network and Computer Applications, vol. 35, 2017, in Press. [Online]. Available: https://goo.gl/uTsQeg no. 3, pp. 1086–1105, 2012. [33] A. Gómez, X. Mendialdua, G. Bergmann, J. Cabot, C. Debreceni, [14] E. Syriani et al., “AToMPM: A Web-based Modeling Environment,” in A. Garmendia, D. S. Kolovos, J. de Lara, and S. Trujillo, “On Invited Talks, Demonstration Session, Poster Session, and ACM Student the Opportunities of Scalable Modeling Technologies: An Experience Research Competition@MoDELS’13, 2013, pp. 21–25. Report on Wind Turbines Control Applications Development,” [15] K. Altmanninger et al., “Amor–towards adaptable model versioning,” in ECMFA’17, 2017, in Press. [Online]. Available: https://goo.gl/surozr MCCM@MoDELS’08, vol. 8, 2008, pp. 4–50. [34] M. Chechik, F. Dalpiaz, C. Debreceni, J. Horkoff, I. Ráth, R. Salay, and [16] F. Schwägerl et al., “Model-based Tool Support for Consistent Three- D. Varró, “Property-Based Methods for Collaborative Model Develop- way Merging of EMF Models,” in ACME@ECOOP’13, 2013, pp. 2:1– ment,” in GEMOC+MPM@MoDELS’15, 2015, pp. 1–7. 2:10. [35] C. Debreceni, G. Bergmann, I. Ráth, and D. Varró, “Property-based [17] J. Rubin and M. Chechik, “N-way Model Merging,” in ACM SIGSOFT Locking in Collaborative Modeling,” in MoDELS’17, 2017, in Press. Symp@ESEC/FSE’13, 2013, pp. 301–311. [36] C. Debreceni, I. Ráth, D. Varró, X. D. Carlos, X. Mendialdua, and [18] P. Brosch et al., “We can work it out: Collaborative Conflict Resolution S. Trujillo, “Automated Model Merge by Design Space Exploration,” in Model Versioning,” in ECSCW’09, 2009, pp. 207–214. in FASE’16, 2016, pp. 104–121. [19] H. K. Dam et al., “Inconsistency Resolution in Merging Versions of [37] H. Abdeen, D. Varró, H. A. Sahraoui, A. S. Nagy, C. Debreceni, Architectural Models,” in WICSA’14, 2014, pp. 153–162. Á. Hegedüs, and Á. Horváth, “Multi-objective Optimization in Rule- [20] U. Mansoor et al., “MOMM: Multi-objective model merging,” Journal based Design Space Exploration,” in ASE ’14, 2014, pp. 289–300. of Systems and Software, vol. 103, pp. 423–439, 2015. [38] C. Debreceni, Á. Horváth, Á. Hegedüs, Z. Ujhelyi, I. Ráth, and [21] H. Song et al., “Instant and Incremental QVT Transformation for D. Varró, “Query-driven Incremental Synchronization of View Models,” Runtime Models,” in MoDELS’11, 2011, pp. 273–288. in VAO@STAF’14, 2014, pp. 31–38. [22] “Towards Automatic Model Synchronization from Model Transforma- [39] O. Semeráth, C. Debreceni, Á. Horváth, and D. Varró, “Change Prop- tions, author=Xiong, Yingfei and others, booktitle=ASE’07, pages=164– agation of View Models by Logic Synthesis using SAT solvers,” in 173, year=2007,.” BX@ETAPS’16, 2016, pp. 40–44. [23] D. S. Kolovos, “Establishing Correspondences between Models with the [40] ——, “Incremental Backward Change Propagation of View Models by Epsilon Comparison Language,” in ECMDA-FA’09, 2009, pp. 146–157. Logic Solvers,” in MoDELS’16, 2016, pp. 306–316. [24] A. Schurr, “Specification of Graph Translators with Triple Graph Gram- mars,” in Graph-Theoretic Concepts in Computer Science, WG’94, 1994, pp. 151–163.