ABSTRACT. Developing complex software requires that multiple views and versions of the software can be developed in parallel and merged as supported by views and managed by version control systems.

In this context, this paper considers monitoring merging and related consistency problems permanently at the level of models and abstract syntax to permit early and frequent conflict detection while developing in parallel. The presented approach introduces multi-version models based on typed graphs that permit to store changes and multiple versions in one graph in a compact form and allow (1) to study well-formedness for all versions without the need to extract each version individually, (2) to report all possible merge conflicts without the need to merge all pairs of versions, and (3) to report all violations of well-formedness conditions that will result for merges of any two versions independent of any merge decisions without the need to merge all pairs of versions.

The paper defines the related concepts and algorithms operating on multi-version models, proves their correctness w.r.t. the usually employed three-way-merge, and reports on preliminary experiments concerning the scalability.

ABSTRACT. The Digital Asset Modelling Language (DAML) enables low-code development of smart contract applications. Starting from a high-level but textual notation, DAML thus implements the lower end of a model-driven development process, from a platform-independent (but technology-oriented) level to implementations on a range of blockchain platforms. % Existing approaches for modelling blockchains and smart contracts support the domain-oriented, conceptual view but do not link to the same technology-specific level.

We provide the missing link, developing a detailed visual design approach based on class diagrams and visual contracts that map directly to DAML smart contracts. The approach is grounded in an operational semantics in terms of graph transformations that account for the more complex behavioral features of DAML, such as its role-based access control and the order of contract execution and archival.

The models, with their mappings to DAML and their operational semantics, are introduced via the Doodle case study from a DAML tutorial.

ABSTRACT. In model-driven optimization (MDO), domain-specific models are used to solve optimization problems with evolutionary algorithms. A graph-based framework for MDO identifies and clarifies its core concepts and relies on mutations as evolutionary change operators. While mutations have been formally defined as graph transformations, no recombination mechanism has been elaborated yet. In this paper, we introduce a generic crossover construction for graph-like structures that can be used to implement recombination operators in MDO. We prove some of the basic properties of our construction (such as its well-definedness) and outline how it can be used to implement a whole range of crossover operators that have been introduced for specific problems and situations on graphs.

ABSTRACT. We demonstrate how category theory provides specifications that can efficiently be implemented via imperative algorithms and apply this to the field of graph rewriting. By examples, we show how this paradigm of software development makes it easy to quickly write correct and performant code. We provide a modern implementation of graph rewriting techniques at the level of abstraction of finitely-presented C-sets and clarify of the connections between C-sets and the typed graphs supported in existing rewriting software. We emphasize that our open-source library is extensible: by taking new categorical constructions (such as slice categories, structured cospans, and distributed graphs) and relating their limits and colimits to those of their underlying categories, users inherit efficient algorithms for pushout complements and (final) pullback complements. This allows one to perform double-, single-, and sesqui-pushout rewriting over a broad class of data structures.

ABSTRACT. The analysis of behavioral models such as Graph Transformation Systems (GTSs) is of central importance in model-driven engineering. However, GTSs often result in intractably large or even infinite state spaces and may be equipped with multiple or even infinitely many start graphs. To mitigate these problems, static analysis techniques based on finite symbolic representations of sets of states or paths thereof have been devised. We focus on the technique of k-induction for establishing invariants specified using graph conditions. To this end, k-induction generates symbolic paths backwards from a symbolic state representing a violation of a candidate invariant to gather information on how that violation could have been reached possibly obtaining contradictions to assumed invariants. However, GTSs where multiple agents regularly perform actions independently from each other cannot be analyzed using this technique as of now as the independence among backward steps may prevent the gathering of relevant knowledge altogether.

In this paper, we extend k-induction to GTSs with multiple agents thereby supporting a wide range of additional GTSs. As a running example, we consider an unbounded number of shuttles driving on a large-scale track topology, which adjust their velocity to speed limits to avoid derailing. As central contribution, we develop pruning techniques based on causality and independence among backward steps and verify that k-induction remains sound under this adaptation as well as terminates in cases where it did not terminate before.

ABSTRACT. Existing graph transformation (GT) tools treat graphs as ephemeral data structures, i.e., the successful application of a GT rule to a graph G rewrites that graph to produce a modified graph G′. The original graph G is lost during that update. In contrast to ephemeral data structures, persistent data structures preserve access to all previ- ous versions when data is modified and fully persistent data structures even allow all previous versions to be modified. In earlier work, we intro- duced the Graph Rewriting and Persistence Engine Grape as a tool for specifying and executing transformations on large-scale graphs and inte- grated it with a computational notebook platform (GrapePress). While the term “persistence” has been in the tool’s acronym from the start, it was chosen to indicate that graphs were maintained in a database with full transactional support. Until now, Grape (and GrapePress) treated graphs as ephemeral data structures, i.e., previous graph versions were not retained upon modification. This paper presents a major revision of the tool to support fully persistent graph rewriting. This tool, called GrapeVine, treats graphs as immutable, first order objects. It therefore more faithfully implements the mathematical theory of GTs.