Incremental static analyses provide up-to-date analysis results in time proportional to the size of a code change, not the entire code base. This promises fast feedback to programmers in IDEs and when checking in commits. However, existing incremental analysis frameworks fail to deliver on this promise for whole-program lattice-based data-flow analyses. In particular, prior Datalog-based frameworks yield good incremental performance only for intra-procedural analyses.

Abstract Studying large-scale collaborative systems engineering projects across teams with differing intellectual property clearances, or healthcare solutions where sensitive patient data needs to be partially shared, or similar multi-user information systems over databases, all boils down to a common mathematical framework. Updateable views (lenses) and more generally bidirectional transformations are abstractions to study the challenge of exchanging information between participants with different read access privileges. The view provided to each participant must be different due to access control or other limitations, yet also consistent in a certain sense, to enable collaboration towards common goals. A collaboration system must apply bidirectional synchronization to ensure that after a participant modifies their view, the views of other participants are updated so that they are consistent again. While bidirectional transformations (synchronizations) have been extensively studied, there are new challenges that are unique to the multidirectional case. If complex consistency constraints have to be maintained, synchronizations that work fine in isolation may not compose well. We demonstrate and characterize a failure mode of the emergent behaviour, where a consistency restoration mechanism undoes the work of other participants. On the other end of the spectrum, we study the case where synchronizations work especially well together: we characterize very well-behaved multidirectional transformations, a non-trivial generalization from the bidirectional case. For the former challenge, we introduce a novel concept of controllability, while for the latter one, we propose a novel formal notion of faithful decomposition. Additionally, the paper proposes several novel properties of multidirectional transformations.

Abstract When custom modeling tools are used for designing complex safety-critical systems (e.g., critical cyber-physical systems), the tools themselves need to be validated by systematic testing to prevent tool-specific bugs reaching the system. Testing of such modeling tools relies upon an automatically generated set of models as a test suite. While many software testing practices recommend that this test suite should be diverse, model diversity has not been studied systematically for graph models. In the paper, we propose different diversity metrics for models by generalizing and exploiting neighborhood and predicate shapes as abstraction. We evaluate such shape-based diversity metrics using various distance functions in the context of mutation testing of graph constraints and access policies for two separate industrial DSLs. Furthermore, we evaluate the quality (i.e., bug detection capability) of different (random and consistent) model generation techniques for mutation testing purposes.

Large-scale model-driven system engineering projects are carried out collaboratively. Engineering artefacts stored in model repositories are developed in either offline (checkout–modify–commit) or online (GoogleDoc-style) scenarios. Complex systems frequently integrate models and components developed by different teams, vendors and suppliers. Thus, confidentiality and integrity of design artefacts need to be protected in accordance with access control policies. We propose a secure collaborative modelling approach where fine-grained access control for models is strictly enforced by bidirectional model transformations. Collaborators obtain filtered local copies of the model containing only those model elements which they are allowed to read; write access control policies are checked on the server upon submitting model changes. We present a formal collaboration schema which provenly guarantees certain correctness constraints, and its adaption to online scenarios with on-the-fly change propagation and the integration into existing version control systems to support offline scenarios. The approach is illustrated, and its scalability is evaluated using a case study of the MONDO EU project.

The article “Enforcing fine-grained access control for secure collaborative modelling using bidirectional transformations”, written by Csaba Debreceni, Gábor Bergmann, István Ráth, Dániel Varró, was originally published electronically on the publisher’s internet portal (https://link.springer.com/journal/10270) on [11/21/2017 6:24:42 AM] without open access.

Program analyses detect errors in code, but when code changes frequently as in an IDE, repeated re-analysis from-scratch is unnecessary: It leads to poor performance unless we give up on precision and recall. Incremental program analysis promises to deliver fast feedback without giving up on precision or recall by deriving a new analysis result from the previous one. However, Datalog and other existing frameworks for incremental program analysis are limited in expressive power: They only support the powerset lattice as representation of analysis results, whereas many practically relevant analyses require custom lattices and aggregation over lattice values. To this end, we present a novel algorithm called DRedL that supports incremental maintenance of recursive lattice-value aggregation in Datalog. The key insight of DRedL is to dynamically recognize increasing replacements of old lattice values by new ones, which allows us to avoid the expensive deletion of the old value. We integrate DRedL into the analysis framework IncA and use IncA to realize incremental implementations of strong-update points-to analysis and string analysis for Java. As our performance evaluation demonstrates, both analyses react to code changes within milliseconds.

Large-scale model-driven engineering projects are carried out collaboratively. Enabling a high degree of concurrency is required to make the traditionally rigid development processes more agile. The increasing number of collaborators increases the probability of introducing conflicts which need to be resolved manually by the collaborators. In case of highly interdependent models, avoiding conflicts by the use of locks can save valuable time. However, traditional locking techniques such as fragment-based and object-based strategies may impose unnecessary restrictions on editing, which can decrease the efficiency of collaboration.In this paper, we propose a property-based locking approach that generalizes traditional locking techniques, and further allows more fine-grained locks in order to restrict modifications only when necessary. A lock is considered to be violated if a match appears or disappears for its associated graph pattern (formula), which captures the property of the model that the upcoming edit transaction can be freely executed. An initial evaluation has been carried out using a case study of the MONDO EU project.

Model-based systems engineering of critical cyber-physical systems necessitates effective collaboration between different stakeholders while still providing secure protection of intellectual properties of all involved parties. While engineering artifacts are frequently stored in version control repositories, secure access control is limited to file-level strategies in most existing frameworks where models are split into multiple fragments with all-or-nothing permissions, which becomes a scalability and usability bottleneck in case of complex industrial models.

The current release of VIATRA provides open-source tool support for an event-driven, reactive model transformation engine built on top of highly scalable incremental graph queries for models with millions of elements and advanced features such as rule-based design space exploration complex event processing or model obfuscation. However, the history of the VIATRA model transformation framework dates back to over 16 years. Starting as an early academic research prototype as part of the M.Sc project of the the first author it first evolved into a Prolog-based engine followed by a family of open-source projects which by now matured into a component integrated into various industrial and open-source tools and deployed over multiple technologies. This invited paper briefly overviews the evolution of the VIATRA/IncQuery family by highlighting key features and illustrating main transformation concepts along an open case study influenced by an industrial project.

Queries are the foundations of data intensive applications. In model-driven software engineering (MDSE), model queries are core technologies of tools and transformations. As software models are rapidly increasing in size and complexity, most MDSE tools frequently exhibit scalability issues that decrease developer productivity and increase costs. As a result, choosing the right model representation and query evaluation approach is a significant challenge for tool engineers. In the current paper, we aim to provide a benchmarking framework for the systematic investigation of query evaluation performance. More specifically, we experimentally evaluate (existing and novel) query and instance model metrics to highlight which provide sufficient performance estimates for different MDSE scenarios in various model query tools. For that purpose, we also present a comparative benchmark, which is designed to differentiate model representation and graph query evaluation approaches according to their performance when using large models and complex queries.

Model-driven development tools built on industry standard platforms, such as the Eclipse Modeling Framework (EMF), heavily use model queries in various use cases, such as model transformation, well-formedness constraint validation and domain-specific model execution. As these queries are executed rather frequently in interactive modeling applications, they have a significant impact on the runtime performance of the tool, and also on the end user experience. However, due to their complexity, they can be time consuming to implement and optimize on a case-by-case basis. To address these shortcomings, we developed the EMF-INCQUERY framework for defining declarative queries over EMF models and executing them effectively using a caching mechanism. In the current paper, we demonstrate how our framework can be easily integrated with other EMF tools. We describe a case study in which EMF-INCQUERY is integrated into the open source Papyrus UML environment to provide on-the-fly validation of well-formedness criteria in UML models.

Model-driven analysis aims at detecting design flaws early in high-level design models by automatically deriving mathematical models. These analysis models are subsequently investigated by formal verification and validation (V&V) tools, which may retrieve traces violating a certain requirement. Back-annotation aims at mapping back the results of V&V tools to the design model in order to highlight the real source of the fault, to ease making necessary amendments. Here we propose a technique for the back-annotation of simulation traces based on change-driven model transformations. Simulation traces of analysis models will be persisted as a change model with high-level change commands representing macro steps of a trace. This trace is back-annotated to the design model using change-driven transformation rules, which bridge the conceptual differences between macro steps in the analysis and design traces. Our concepts will be demonstrated on the back-annotation problem for analyzing BPEL processes using a Petri net simulator.