The Verigraph system for graph transformation

Abstract

Graph transformation (GT) is a rule-based framework, suitable for modelling both static and dynamic aspects of complex systems in an intuitive yet formal manner. The algebraic approach to GT is based on category theory, allowing the instantiation of theoretical results to multiple graph-like structures (e.g. labelled or attributed graphs, Petri nets, even transformation rules themselves). There exists a rich theory of algebraic GT which underlies verification techniques such as static analysis. Current tools based on GT are implemented in a very concrete way, unlike the theory, making them hard to extend with novel theoretical results. Thus a new software system called Verigraph was created, with the goal of implementing the theory as closely as possible, while maintaining a reasonable execution time. In this paper we present the architecture of Verigraph, which enabled an almost direct implementation of the theory. We also provide a step-by-step guide to implementing a new graph model within the system, using second-order graph transformation as an example. Finally, we compare the performance of Verigraph and AGG.