Advertisement

Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions

  • Sven SchneiderEmail author
  • Johannes Dyck
  • Holger Giese
Conference paper
  • 68 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12150)

Abstract

The behavior of various kinds of dynamic systems can be formalized using typed attributed graph transformation systems (GTSs). The states of these systems are then modelled using graphs and the evolution of the system from one state to another is described by a finite set of graph transformation rules. GTSs with small finite state spaces can be analyzed with ease but analysis is intractable/undecidable for GTSs inducing large/infinite state spaces due to the inherent expressiveness of GTSs. Hence, automatic analysis procedures do not terminate or return indefinite or incorrect results.

We propose an analysis procedure for establishing state-invariants for GTSs that are given by nested graph conditions (GCs). To this end, we formalize a symbolic analysis algorithm based on k-induction using Isabelle, apply it to GTSs and GCs over typed attributed graphs, develop support to single out some spurious counterexamples, and demonstrate the feasibility of the approach using our prototypical implementation.

Keywords

Formal static analysis Symbolic state space abstraction k-induction Symbolic graphs Isabelle 

1 Introduction

The verification of formal models of complex dynamic systems w.r.t. to formal specifications is one of the grand challenges of model driven engineering. However, the expressiveness required to cover the multitude of complex actual and desired behaviors of such systems renders analysis often undecidable. Indeed, the formalism of graph transformation systems (GTSs) considered here is known to be Turing complete. Hence, fully-automatic procedures for establishing meaningful properties on the behavior of such systems are then guaranteed to be not terminating in general or to produce indefinite or even incorrect results. We subsequently focus on GTSs where an analysis using an explicit state space exploration using tools such as Open image in new window  [2] and Open image in new window  [3] is not applicable due to infinite or intractably large sets of initial or reachable states.

We approach this problem by combining the symbolic static analysis techniques of k-induction and state abstractions to establish state invariants for dynamic systems with infinite state spaces modelled by GTSs. The idea of k-induction is to establish a state invariant by iteratively computing all shortest derivations from an initial state to a violating state. The use of state abstractions, which preserve and reflect the systems’ behavior w.r.t. the invariant candidate, permits to handle GTSs with infinite sets of initial or violating states at the concrete level but finite (and sufficiently small) such sets at the abstract level.

As main contributions, we (a) formalize the principle of k-induction in the theorem prover Isabelle in the form of an analysis algorithm and (b) instantiate this analysis algorithm for the setting of (b1) invariant candidates formalized using the logic of nested graph conditions ( Open image in new window ) and (b2) a suitable notion of typed attributed graph transformation. This instantiation based approach thereby also clearly separates aspects of k-induction from GTS related concepts.

To represent typed attributed graphs, we employ symbolic graphs [18, 19, 20, 21, 22], which are similar to Open image in new window  [12]. These symbolic graphs also give rise to an instantiation of Open image in new window that permits the specification of constraints on attributes throughout the Open image in new window . We employ a graph transformation step relation on symbolic graphs that deviates from those formalized in [21, 22] by being symmetric (allowing a backwards application used in the k-induction analysis algorithm) and by allowing for the removal of variables (not requiring that additional variables and their values must be guessed when computing backward steps).

As closest related work, approaches using k-induction have been used before without formal foundation in [4] and in [7, 8, 9, 10, 11] assuming \(k=1\), graphs without attributes, a single initial state, or a subclass of all Open image in new window . Hence, we extend this line of research by formally treating the more general case of an arbitrary value of k, graphs with attributes, infinitely many initial states, and all Open image in new window .

In [5, 25, 27, 28], an abstraction of graphs results in shape graphs (which have limited expressiveness compared to Open image in new window ) where multiple nodes in the graph are represented by so called summary nodes in the shape graph and where multiplicity or even first-order logic constraints may further restrict this abstraction (see also [6]). Moreover, in [15], an abstraction of graphs is given in terms of consistent compasses (which can be encoded in Open image in new window of depth one) containing a set of graphs of which one is matchable and a set of non-matchable graphs. Also, in [29], the tool Open image in new window is used to establish state invariants for typed graphs.

Further related analysis approaches are as follows. The tool Open image in new window  [1] abstracts GTSs to Petri nets but imposes restrictions on graph transformation rules thereby limiting expressiveness. Lastly, static analysis of programs for GTSs w.r.t. pre/post conditions has been developed in [23] as well as [24].

In Sect. 2, we formalize the principle of k-induction in the form of an analysis algorithm. In Sect. 3, we discuss our running example, our notion of attributed graph transformation, and the logic of Open image in new window . In Sect. 4, we instantiate the analysis algorithm for attributed graph transformation and apply our prototypical implementation of it to our running example demonstrating its feasibility. In Sect. 5, we provide a conclusion and a discussion of future work.

2 Invariant Verification Using k-Induction

We now introduce our formalization of the technique of k-induction for the verification of (state) invariants. For this purpose, we introduce labelled transition systems (LTS) as an abstract framework, which is instantiated later on for graph transformation. The results of this section have been formalized in the interactive theorem prover Isabelle and we therefore omit all proofs. An LTS consists of a set S of states, a set L of labels, a relation \(\delta \) of labelled steps between states, and initial states identified via a state predicate Z.

Definition 1

(Labelled Transition System (LTS)). If S and L are sets of states and labels, \(\delta \subseteq S\times L\times S\), Open image in new window and \(\varGamma =(S,L,\delta ,Z)\), then \(\varGamma \) is a labelled transition system, written Open image in new window.

Moreover, a finite path Open image in new window of \(\varGamma \) of length n is a sequence of n states from S interleaved with labels from L where \(s\cdot l\cdot s'\) in \(\pi \) implies \((s,l,s')\in \delta \). Also, Open image in new window and Open image in new window map indices to the states and labels of the path \(\pi \).

In Sect. 4, we restrict the states of an LTS resulting in a sub-LTS as follows.

Definition 2

(Sub-LTS). If Open image in new window, \(S'\subseteq S\), and Open image in new window, then \(\varGamma '\) is a sub-LTS of \(\varGamma \).

A predicate I on the states of an LTS is an invariant for the LTS, if all states that are reachable from an initial state of the LTS satisfy I.

Definition 3

(Invariant). If Open image in new window, Open image in new window, and Open image in new window Open image in new window, then \(\varGamma \) has invariant I, written Open image in new window.

Subsequently, we assume an invariant A (e.g. expressing earlier established invariants) for the LTS to improve applicability of the analysis approach as explained later on. For characterizing the k-induction algorithm below, we define shortest violations of a state predicate I as a finite path leading from an initial state to a state violating I visiting no further initial states and only passing through states satisfying I as well as A.

Definition 4

(Shortest Violation). If Open image in new window , and Open image in new window , then \(\pi \) is a shortest violation of I by \(\varGamma \) of length k under A, written Open image in new window .

The analysis algorithm \({\mathcal {I}}\) below checks for such shortest violations by (a) selecting all violating states s satisfying \(\lnot I(s)\) and by (b) computing up to k steps backwards ensuring that all k additional states \(s'\) visited on each of the paths obtained satisfy \(A(s')\wedge I(s')\). Firstly, when a state \(s'\), which is visited in this process, satisfies \(Z(s')\), a shortest violation is obtained. Secondly, when no such path of k steps exists, there cannot be a shortest violation of greater length. Note that this analysis process benefits from employing the assumed invariant A, which is used to rule out paths with states that are known to be unreachable from an initial state by not satisfying A.

The analysis algorithm \({\mathcal {I}}\) returns a value b with three different values where \(b=\mathsf {i}\) represents a successful verification of the given state predicate I as an invariant (when no paths are left that may be extended to shortest violations), where \(b=\mathsf {v}\) represents that at least one shortest violation was determined, and where \(b=\mathsf {u}\) represents the situation that the analysis was unable to return one of the two former definite results for the provided value of k that is decremented in each recursive application of \({\mathcal {I}^{\mathrm {inner}}}\).

Definition 5

(\({{\mathcal {I}}}\)). If Open image in new window then Open image in new window as follows.Moreover, if Open image in new window and Open image in new window is the set of violating paths of length 0, then Open image in new window.

The following theorem states that the analysis algorithm \({\mathcal {I}}\) performs a sound state invariant analysis as just described above.

Theorem 1

(Soundness of \({{\mathcal {I}} {}}\)). If Open image in new window , and Open image in new window , then there is Open image in new window and one of the following items holds.

The analysis algorithm \({\mathcal {I}}\) is implementable when the set of paths considered is finite throughout its computation. This is guaranteed when the LTS has violations for at most finitely many states (finite initial set of paths handed to \(\mathcal {I}^\text {inner}\)) and when every state has at most finitely many predecessors (each path can only be extended backwards to finitely many paths in \(\mathcal {I}^\text {inner}\)).

Definition 6

(Finitely Backwards Branching LTS). If Open image in new window , and Open image in new window , then \(\varGamma \) is finitely backwards branching for I.

The concrete instantiation of LTSs for GTSs in Sect. 4 is not finitely backwards branching in general because invariant candidates I may be violated by infinitely many states. Hence, we apply in Sect. 4 an abstraction leading to an abstract instantiation of LTSs for GTSs where the corresponding invariant candidate \(I'\) is violated by finitely many states. We then establish a connection between both instantiations in terms of an LTS abstraction relation (LTSAR), which permits to analyze the abstract instantiation using \({\mathcal {I}}\) instead of the concrete instantiation.

Intuitively, the paths considered using \({\mathcal {I}}\) for the concrete LTS are symbolically represented by the finite set of paths considered using \({\mathcal {I}}\) for the abstract LTS. Formally, an LTSAR consists of two subrelations \(R_S\) relating states and \(R_L\) relating labels of the underlying concrete and abstract LTSs. Note that we state suitable requirements on the relations \(R_S\) and \(R_L\) of an LTSAR in the following theorem and define only the type of an LTSAR here.

Definition 7

(LTS Abstraction Relation (LTSAR)). If Open image in new window , then \((R_S,R_L)\) is an LTS Abstraction Relation from \(\varGamma \) to \(\varGamma '\), written Open image in new window .

For invariant candidates I and \(I'\) for \(\varGamma \) and \(\varGamma '\), the following theorem states six requirements on an LTSAR \((R_S,R_L)\), which guarantee that (a) a violation of \(I'\) in \(\varGamma '\) implies the existence of a violation of I in \(\varGamma \) and (b) the absence of violations of \(I'\) in \(\varGamma '\) implies the absence of violations of I in \(\varGamma \).

Theorem 2

(Preservation/Reflection of Invariants using LTS Abstraction Relations). If Open image in new window and Open image in new window , then both of the following items hold.

The requirements R1–R6 used in these items are as follows.

  • R1: Open image in new window(\(R_S\) is compatible with invariant satisfaction)

  • R2: Open image in new window(\(R_S\) is compatible with initial states)

  • R3: Open image in new window

    ( \(R_S\) relates a concrete state \(s\in S\) to each abstract state \(s'\in S'\) )

  • R4: Open image in new window (\(R_S\) relates an abstract state \(s'\in S'\) to each concrete state \(s\in S\) for which a shortest violation of I exists)

  • R5: Open image in new window

    (every forward step of the abstract LTS \(\varGamma '\) can be mimicked (forwards) by the concrete LTS \(\varGamma \) for two related source states \((s,s')\) to allow for the concretization of a violating path)

  • R6: Open image in new window(every backward step of the concrete LTS \(\varGamma \) (except for those leading to initial states) can be mimicked (backwards) by the abstract LTS \(\varGamma '\) for two related target states \((\bar{s},\bar{s}')\) to allow for the abstraction of a violating path)

3 Modelling and Specifying Graph Transformation

As a running example, we consider a single shuttle travelling on a network of tracks (see Fig. 1a for the type graph used) where subsequent tracks are connected using next edges. The graph attribution stores the velocity v and acceleration a of the shuttle and, moreover, the constants for minimal, maximal, and safe velocities as well as the constant track length s in a System node. The rules refer to the attributes to describe the velocity \(v'\) of a shuttle after travelling over a track based on its current velocity v, acceleration a, and the constant track length s using the standard equation \(v'^2=v^2+2as\). The velocity of the shuttle should be below the safe velocity on tracks with flag signal, the velocity of the shuttle should be constant on tracks with flag const, and the flag warning on a track indicates that a track with flag signal is to be expected ahead. Analysis should establish the fact that the shuttle never violates signal and const flags as an invariant, which is formalized in Fig. 1c using graph conditions explained below. Note that tracks with flag const between tracks with flag warning and tracks with flag signal may prevent timely deceleration. We employ an assumed invariant to (a) specify the constant attribute values of the system node, (b) to rule out track networks with dead ends and loops, and (c) to ensure warnings n tracks ahead of signals for a parameter Open image in new window in all considered track networks.
Fig. 1.

Type graph and invariant candidate for the shuttle scenario.

We now recall attribute conditions ( Open image in new window ) used by symbolic graphs and then revisit GTSs and Open image in new window over symbolic graphs for describing actual and desired behavior in terms of a concrete LTS and state predicates from before.

The attribute logic AL contains Open image in new window of first-order logic (FOL) ranging over a set X of variables. The satisfaction of Open image in new window by a valuation Open image in new window is denoted by Open image in new window . The Open image in new window solver Open image in new window  [17] supports Open image in new window constructed using a restricted set of operators for the sorts Open image in new window . When Open image in new window is unable to determine an answer to the satisfiability problem (note that Open image in new window satisfaction is undecidable), which does not occur for the examples considered here, we would notify the user in our prototypical implementation.

Symbolic graphs (called graphs subsequently) [18] are an adaptation of Open image in new window  [12]. A finite graph G (such as those depicted in Fig. 1b) contains nodes, edges, variables Open image in new window, and an AC Open image in new window ranging over Open image in new window . Moreover, nodes and edges are equipped with node and edge attributes, which are connected to variables for which values are specified in the AC Open image in new window . A morphism Open image in new window from graph \(G_1\) to \(G_2\) (see e.g. Fig. 1b) maps nodes, edges, variables, node attributes, and edge attributes of \(G_1\) to those of \(G_2\). The mappings of m must be compatible with the source and target functions of \(G_1\) and \(G_2\) as usual and Open image in new window must imply the translation Open image in new window of Open image in new window for all variable valuations to ensure that m characterizes a restriction of attributes (cf. Fig. 1b where this implication is discussed). Moreover, the class of all finite graphs typed (as usual using a typing morphism) over a given type graph  Open image in new window is given by Open image in new window or simply Open image in new window when Open image in new window is known. In the remainder, we only employ monomorphisms, written Open image in new window, with only injective mappings. The unique monomorphism from the empty graph Open image in new window to a graph G is denoted Open image in new window. Finally, the special monomorphism Open image in new window describes that \(G'\) is obtained from G by setting the Open image in new window to true (i.e., \(G'\) equals G except that Open image in new window ).

The graph logic GL [14, 26] supports the specification of the (non)existence of certain subgraphs in a given host graph G. Besides propositional operators for (finite) conjunction and negation, GL features the Open image in new window operator Open image in new window , which specifies for a given match Open image in new window of a (context) graph H into the host graph G that m can be extended to a match Open image in new window by using a monomorphism Open image in new window that explains how H is extended to the (context) graph \(H'\).

The graph \(G_2\) from Fig. 1b does not satisfy Open image in new window because the initial monomorphism Open image in new window can be extended to m from Fig. 1b, which is forbidden by the left part Open image in new window of Open image in new window.

Definition 8

(Graph Logic (GL)). If Open image in new window is a finite graph, Open image in new window is a monomorphism, then Open image in new window is a graph condition over H, written Open image in new window , which is satisfied by m, written Open image in new window

Moreover, we define the following notions.

Moreover, we define that two Open image in new window and Open image in new window are consistent, when Open image in new window only describes elements also described by Open image in new window or none of them.

To check satisfiability of a GC and consistency of two Open image in new window , we employ the automated reasoning technique for GL in the form of the algorithm Open image in new window for which tool support is available in Open image in new window as introduced in [26]. The algorithm Open image in new window takes a GC Open image in new window as input, is known to terminate for unsatisfiable Open image in new window (i.e., it is refutationally complete), and incrementally generates the set of minimal graphs satisfying Open image in new window (this set is empty for unsatisfiable Open image in new window ). As for the case of Open image in new window and Open image in new window , we carefully handle cases where Open image in new window does not terminate and also generates no minimal graph as discussed later on.

Fact 1

(Algorithm \(\mathcal {A}\)). If Open image in new window is a GC over the empty graph and Open image in new window terminates for Open image in new window , it returns the finite set of all minimal graphs satisfying  Open image in new window .

The standard operation Open image in new window from [13] is also applicable to symbolic graphs [26]. It defines an adaptation of a GC Open image in new window with context graph H for a monomorphism Open image in new window resulting in an equivalent GC with context graph \(H'\) in the sense of the following fact (by considering how additional elements of \(H'\) may be used in a satisfaction proof for the given GC Open image in new window).

Graph transformation steps are defined using rules specifying structural and attribute transformations. A rule Open image in new window contains for the structural part (as in the DPO approach) two monomorphisms Open image in new window where K, Open image in new window , and Open image in new window contain the preserved/deleted/added elements. For the attribute part, L, K, and R have the trivial Open image in new window and a rule Open image in new window contains an Open image in new window instead, which is defined over the disjoint union V (i.e., the coproduct, written  Open image in new window where Open image in new window and Open image in new window map variables to the disjoint union V) of the variables of L and R. Intuitively, variables originating from L are used as unprimed variables and variables originating from R are used as primed variables. Finally, a rule contains left and right hand side application conditions Open image in new window and Open image in new window defined over the graphs L and R and checked during the transformation as in the DPO approach. See Fig. 3 for two simple rules1 and, for our running example, Fig. 2 for two of the total nine rules (see [8, Section C.1.6, p. 336] for a full description of the assumed invariants and rules of the considered GTS).
Fig. 2.

Two rules and a graph transformation sequence for our shuttle scenario.

Fig. 3.

Example of invariant analysis for abstract LTS.

Definition 10

(Graph Transformation Rules). If Open image in new window are to monomorphisms, Open image in new window is a coproduct, Open image in new window , and Open image in new window , then Open image in new windowis a rule, written Open image in new window .

Moreover, we define the following abbreviations.

Graph transformations systems then contain a finite set of finite rules (used for graph transformation steps) and initial states described by a GC.

Definition 11

(Graph Transformation System (GTS)). If Open image in new window and Open image in new window , then Open image in new windowis a graph transformation system.

Deviating from [22], we now introduce a notion of graph transformation steps in which structural and attribute transformations are decoupled. The defined step relation is symmetric and supports the removal as well as addition of variables, which is also relevant when attribute values are to be modified.

Definition 12

(Steps). There is a step Open image in new window with label Open image in new window , whenever

For this construction, Open image in new window is the used label where Open image in new window is the derived rule (cf. [13]) with Open image in new window and where the Open image in new window is adapted from Open image in new window according to the renamings of \(c_1\) and \(c_2\).

For our running example, see Fig. 2c for a graph transformation sequence applying the two rules from Fig. 2a and Fig. 2b. Note that the last graph of this sequence violates the invariant candidate from Fig. 1c as the shuttle exceeds the permitted velocity on a track with signal flag.

The steps defined by this construction immediately induce a concrete LTS (see Definition 1) for a given GTS where the initial states are given by all graphs satisfying the GC characterizing initial graphs of the GTS.

Definition 13

(Concrete LTS of Graph Transformation). If Open image in new window is a GTS then Open image in new windowis the concrete LTS ofOpen image in new window with

Moreover, a state G of \(\varGamma \) (i.e., a finite graph) satisfies a state predicate (cf. the last item above) given by a GC Open image in new window defined over the empty graph Open image in new window iff Open image in new window .

Finally, the operations Open image in new window and the reverse operation Open image in new window introduced in [13] can be adapted to symbolic graphs. The operation Open image in new window inductively propagates a GC Open image in new window over the right hand side graph Open image in new window (such as the application condition Open image in new window) of a rule Open image in new window to the left hand side graph Open image in new window of Open image in new window by applying the renaming of graph elements according to Open image in new window and Open image in new window to the graphs in the GC Open image in new window. The two operations ensure the following compatibility with steps (cf. [13]).

Fact 3

(Operations Open image in new window and Open image in new window ). If Open image in new window is a finite rule with the left and right hand side graphs L and R, Open image in new window and Open image in new window are Open image in new window over L and R, and Open image in new window is a graph transformation step, then Open image in new window iff Open image in new window and Open image in new window iff Open image in new window .

4 Invariant Analysis for Graph Transformation Systems

Based on the preliminaries from the previous section on graph transformation and graph specification using Open image in new window , we now apply our theory on k-induction from Sect. 2. Note that the instantiation presented here is specific to the step relation for graph transformation presented in the previous section due to the decoupling of transformation of structure and ACs. For this instantiation, we construct an LTS that is finitely backwards branching (see Definition 6) and that is related to the concrete LTS \(\varGamma \) from the previous section via a suitable LTSAR (see Definition 7) to permit an application of Theorem 2 for enabling the analysis of the GTS using \({\mathcal {I}}\) according to Theorem 1. For this purpose, we assume a fixed GTS Open image in new window , the induced LTS Open image in new window (see Definition 13), an assumed invariant Open image in new window , and an invariant candidate Open image in new window .

For demonstration purposes, we consider the GTS Open image in new window with assumed invariant Open image in new window and invariant candidate Open image in new window from Fig. 3.

As an initial candidate for the LTS to be constructed, we define the LTS \(\varGamma '\) in which each state Open image in new window is given by a GC Open image in new window and the graph \(\bar{G}\) over which Open image in new window is defined for improved readability. The LTS \(\varGamma '\) induces an LTSAR in which the relation \(R_S\) contains pairs Open image in new window for which some monomorphism Open image in new window with Open image in new window exists. The steps of \(\varGamma '\) adapt states Open image in new window to states Open image in new window using a rule Open image in new window of the GTS Open image in new window for matches Open image in new window and Open image in new window at the abstract level by considering all concrete steps of graphs \(H_1\) and \(H_2\) that are related to \(G_1\) and \(G_2\) via \(R_S\) (by means of instantiation morphisms \(m_1\) and \(m_2\)). That is, the same rule Open image in new window can be applied to each graph covered by Open image in new window and, vice versa, Open image in new window covers only the graphs reachable using such steps.

Definition 14

Moreover, a state Open image in new window of \(\varGamma '\) satisfies a state predicate (cf. the last item above) given by a GC Open image in new window defined over the empty graph Open image in new window iff Open image in new window.2

We state that each sub-LTS \(\varGamma ''\) of \(\varGamma '\) induces a certain LTSAR for the LTS \(\varGamma \).

Lemma 1

(LTSAR for GTS). If Open image in new window is a GTS, Open image in new window, \(\varGamma ''\) is a sub-LTS of Open image in new window, Open image in new window, and Open image in new window, then Open image in new window by Definition 7.    \(\square \)

Selecting the entire LTS \(\varGamma ''=\varGamma '\) results in an LTSAR, which does not satisfy the requirements of Theorem 2 in general. Instead, we obtain a suitable sub-LTS \(\varGamma ''\) of \(\varGamma '\) in an on-the-fly manner during an application of \({\mathcal {I}}\) (see Definition 5): \(\varGamma ''\) then describes precisely the paths maintained by \({{\mathcal {I}^{\mathrm {inner}}}}\) in its parameter Open image in new window at any point in the computation. Hence, the initial candidate is the sub-LTS \(\varGamma ''_0\) that contains the single state Open image in new window violating Open image in new window . Note that \(\varGamma ''_0\) induces an LTSAR satisfying the requirements R1–R5 already. See Fig. 3f where node \(X_0\) represents this initial state inducing the path \(\pi _0\) of length 0.

Inside an application of Open image in new window (see Definition 5), we extend paths in Open image in new window w.r.t. \(\varGamma '\) and thereby adapt \(\varGamma ''_i\) to \(\varGamma ''_{i+1}\) such that the LTSAR for \(\varGamma ''_{i+1}\) (see Lemma 1) also satisfies the requirements R1–R5 of Theorem 2. The satisfaction of requirement R6 for the backwards simulation may require that further path extensions are computed in subsequent iterations of \({{\mathcal {I}^{\mathrm {inner}}}}\). In Fig. 3f, the path \(\pi _0\) is extended to paths \(\pi _1\) and \(\pi _2\) where the last nodes \(X_2\) and \(X_5\) are then incrementally more specific than \(X_0\) (w.r.t. the monomorphisms that satisfy their Open image in new window ).

When the application of \({\mathcal {I}}\) terminates with a definite result \(b\in \{\mathsf {i},\mathsf {v}\}\), the obtained sub-LTS \(\varGamma ''_i\) constructed up to this point induces an LTSAR, which meets the relevant requirements listed in Theorem 2. In particular (see also Theorem 3 later on), (a) for the result Open image in new window meaning that the invariant candidate Open image in new window is violated by \(\varGamma '\), we can apply Part1 of Theorem 2 because R1–R5 are satisfied and (b) for the result \((\mathsf {i},\emptyset )\) meaning that Open image in new window is established as an invariant for \(\varGamma '\), we can apply Part2 of Theorem 2 because there are no further backward steps that require consideration since all paths constructed so far were discarded for not having any further relevant step implying also R6 as required.

In the remainder, we discuss the backwards construction of paths of \(\varGamma '\) for a GTS using the operation Open image in new window . This extension operation (see Definition 16) entails a refining operation Open image in new window (see Definition 15) used to adapt paths in line with the operation Open image in new window used in \({\mathcal {I}}\) to ensure that the requirements R1–R5 are satisfied by the corresponding sub-LTS \(\varGamma ''_{i+1}\) constructed so far.

Extending a path \(\pi \) of \(\varGamma '\) starting in a state Open image in new window adding a backwards step for a rule Open image in new window may result in a refinement due to (a) additional graph elements when the comatch of the step does not only match elements of \(\bar{G}\), (b) additional restrictions originating from the application conditions of Open image in new window, and (c) fewer variable valuations satisfying the AC of the start graph of the path.

For example, in Fig. 3f, the path Open image in new window (in the second line) is refined to Open image in new window according to the monomorphism Open image in new window for the application of Open image in new window in Extension-Step 2. Considering the elements \(X_1\) and \(X_4\) given in more detail in Fig. 3g, we see that \(X_4\) is much more specific than \(X_2\) due to the additional GC originating from Open image in new window, the inclusion of node c and edge e, and a more restrictive AC.

The following operation Open image in new window refines the path \(\pi \) starting in Open image in new window to a path \(\pi '\) starting in Open image in new window for a monomorphism Open image in new window and a GC Open image in new window defined on \(\bar{ X}\), which describe the effect of the backwards step on \(\pi \). It does so by adapting the monomorphisms contained in the labels of the steps in \(\pi \), performs a step leading to a graph \(\bar{ Y}\) to propagate attribute restrictions given by the AC of \(\bar{ X}\), and propagates the additional GC Open image in new window to the resulting graph \(\bar{ Y}\).

Concrete violating paths of \(\varGamma \) (such as in Fig. 2c for our running example) can be constructed from symbolic violating paths of \(\varGamma '\) starting in Open image in new window by (a) running the algorithm Open image in new window from Fact 1 to obtain some monomorphism Open image in new window satisfying Open image in new window , (b) employing Open image in new window to determine a variable valuation satisfying the AC of \(\bar{ X}\) resulting in some monomorphism Open image in new window , and (c) applying the operation Open image in new window for \(m'\) and Open image in new window . Besides such concrete violating paths, we return all symbolic violating paths to the user for which Open image in new window or Open image in new window fail to determine definite results (which does not occur in the examples considered here).

We now introduce the operation Open image in new window for extending a path of \(\varGamma '\) by adding a further backwards step. To ensure that we construct all paths, we follow the definition of E-concurrent rules from [13] to generate all minimal overlaps for each successive rule application and to adjust Open image in new window to the application conditions of the rules. Moreover, in item (8), we employ the operation Open image in new window to adapt the given path of \(\varGamma '\) to the additional step. Finally, in item (9), item (10), and item (11), we further split and filter the constructed paths to ensure that the state predicate satisfaction is compatible with \(R_S\) (see Theorem 3).

Definition 16

(Extension of Abstract Paths). If Open image in new window is a GTS, Open image in new window , then Open image in new window computes the possibly empty set of all path extensions Open image in new window of \(\pi \) using the following procedure.

  1. (1)

    Open image in new window is the first state of \(\pi \).

     
  2. (2)
     
  3. (3)

    Open image in new window is a minimal overlapping of R and \(\bar{G}\) (cf. [13]).3

     
  4. (4)

    Open image in new window is a step of the GTS where Open image in new window is reversed using Open image in new window and applied forwards to E using match \(e_1\) to obtain the required backwards step.

     
  5. (5)

    Open image in new window is the GC for \(\bar{ X}\) obtained using GC propagation as in [13].

     
  6. (6)

    Open image in new window is a step of the GTS using the rule Open image in new window possibly further restricting the AC from E to \(\bar{ Y}\).

     
  7. (7)

    Open image in new window is the GC for \(\bar{ Y}\) obtained using GC propagation as in [13].

     
  8. (8)
    Open image in new window is obtained by prepending the new step to the path refinement of \(\pi \) according to \(\bar{ m}\circ e_2\) and Open image in new window.
     
  9. (9)

    (Disambiguation of Abstraction for Open image in new window) If Open image in new window is consistent with Open image in new window (see Definition 8), which can be checked using Open image in new window , we know that Open image in new window either only covers graphs satisfying Open image in new window or no such graphs. In this case, \(\tilde{\pi }_1\) is Open image in new window or Open image in new window (where Open image in new window is the identity morphism on \(\bar{ X}\)) and \(\tilde{\pi }_1=\tilde{\pi }\) otherwise.

     
  10. (10)

    (Disambiguation of Abstraction for Open image in new window) Analogous to item (9) for the GC Open image in new window representing the initial state of the GTS at hand obtaining \(\tilde{\pi }_2\) from \(\tilde{\pi }_1\).

     
  11. (11)

    (Nonemptyness of Abstraction) If Open image in new window and Open image in new window determine that \(\tilde{\pi }_2\) represents at least one concrete violation (as discussed subsequent to Definition 15) compatible with \(\phi _A\), then \(\pi '\) is equal to \(\tilde{\pi }_2\) (otherwise \(\tilde{\pi }_2\) results in no path extension).

     

Figure 3f depicts two applications of Open image in new window both requiring applications of Open image in new window (the first refinement regarding the empty path \(\pi _0\) is trivial and the second has been discussed above). The first extension uses Open image in new window from Fig. 3a, constructs the overlapping \(E_0\) where the two B nodes are identified (not explicitly depicted), applies the reversal of rule Open image in new window using the match \(e_{01}\) to obtain \(X_1\), and then applies Open image in new window to obtain the AC refinement Open image in new window of \(E_0\) depicted in Fig. 3g. Note that Open image in new window still violates the invariant candidate Open image in new window (for all monomorphisms Open image in new window). The further extension using Open image in new window then results in path \(\pi _2\) ending in Open image in new window , which does not need to be considered further as \(X_5\) violates the assumed invariant Open image in new window (for all monomorphisms Open image in new window).

Finally, \({\mathcal {I}}\) from Definition 5 can be used to check a GTS against an invariant candidate Open image in new window by applying \({{\mathcal {I}}}\) using the described instantiation.

Theorem 3

(Instantiation of k-Induction for GTSs). If Open image in new window is a GTS, Open image in new window is an assumed invariant, Open image in new window is an invariant candidate, Open image in new window , and the application of the algorithm Open image in new window using the described instantiation \(\varGamma '\) for \(\varGamma \), Open image in new window (from Definition 16) for Open image in new window , and Open image in new window terminates with Open image in new window , then Theorem 1 and Theorem 2 are applicable and Open image in new window is a sound judgement on whether Open image in new window is an invariant for Open image in new window.

Table 1.

Results of invariant analysis for the abstract LTS for shuttle scenario.

Outcome Open image in new window of analysis algorithm \({\mathcal {I}}\)

Lookahead n

Path length k

Duration

Element b

Size of element Open image in new window

2

2

1 s

\(\mathsf {u}\)

6

3

3

2 s

\(\mathsf {u}\)

12

4

4

12 s

\(\mathsf {u}\)

8

5

5

63 s

\(\mathsf {i}\)

0

Proof

The used operation Open image in new window for path extension ensures that the last computed sub-LTS \(\varGamma ''\) of \(\varGamma '\) results in an LTSAR (see Lemma 1) meeting the requirements R1–R5 from Theorem 2 as follows (by induction on the parameter k for R4).

  • Requirements R1 and R2 (preservation of invariant and initial state): Ensured by item (9) and item (10) in Definition 16.

  • Requirement R3 (\(R_S\) is right total): Ensured by item (11) in Definition 16.

  • Requirement R4 (\(R_S\) is left total on violating states): R4 means that each state G that violates Open image in new window in \(\varGamma \) via some shortest violation is covered by some state Open image in new window of \(\varGamma ''\). R4 is obviously satisfied by the initial LTS candidate that has the only state Open image in new window . Moreover, every extension (entailing the described refinement) of the set of paths in each iteration preserves this property because the refinement only excludes paths that are known to be only covering paths not representing shortest violations.

  • Requirement R5 (forward steps of \(\varGamma '\) are simulated by \(\varGamma \)): Ensured by applying the path refinement operation Open image in new window in the operation Open image in new window .

Lastly, the requirement R6 is satisfied for all states that are not at the beginning of a path in \(\varGamma ''\) since Open image in new window considers all possible backward steps.   \(\square \)

For our running example, we applied our prototypical implementation of the analysis algorithm \({\mathcal {I}}\). For \(k=2\), we obtained the indefinite result Open image in new window where the sequence from Fig. 2c is a concretization of a path in Open image in new window that could not be ruled out. As stated in Table 1, a path length of \(k=5\) (i.e., 5-induction) was required to establish that Open image in new window is an invariant. While the time required for invariant analysis increases exponentially with longer values of k due to the exponentially increasing number of paths of that length, we believe that the analysis times required for the running example already demonstrate feasibility albeit a potential for further optimizations of our prototypical implementation. Also note that the number of path extensions in each step grows exponentially with the size of the rules.

5 Conclusion and Future Work

We formalized the static analysis approach of k-induction using Isabelle for the abstract setting of LTSs establishing sufficient conditions for the preservation/reflection of invariants by means of an abstraction relation. We then applied this analysis approach to typed attributed GTSs by abstracting graphs by nested graph conditions (GCs) and by applying k-induction on these GCs. Our results extend the state of the art by permitting attributes as well as nested GCs for the specification of initial states, assumed invariants, and invariant candidates.

In the future, we want to develop support for probabilistic/timed GTSs such as [16]. Moreover, we strive to develop further abstractions to improve support for GTSs with multiple active components such as shuttles. Finally, heuristics guiding the computation of paths in the analysis procedure using parameterizations may improve performance by e.g. prioritizing path extension over checking for violations of attribute constraints of assumed invariants.

Footnotes

  1. 1.

    Here, L, K, and R are given in a single graph and preserved/deleted/added elements are colored black/red/green and deleted/added elements are marked with \(\ominus \)/\(\oplus \).

  2. 2.

    Definition 16 resolves cases where Open image in new window and Open image in new window are not consistent (Definition 8).

  3. 3.

    Open image in new window denotes the set of pairs of monomorphisms that are jointly epimorphic, that is, two monomorphisms that map to each graph element of their common target graph.

References

  1. 1.
  2. 2.
    Graphs for Object-Oriented Verification (GROOVE) (2011). http://groove.cs.utwente.nl
  3. 3.
  4. 4.
    Becker, B., Giese, H.: On safe service-oriented real-time coordination for autonomous vehicles. In: 11th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2008), 5–7 May 2008, Orlando, Florida, USA, pp. 203–210. IEEE Computer Society (2008).  https://doi.org/10.1109/ISORC.2008.13
  5. 5.
    Boneva, I., Rensink, A., Kurbán, M.E., Bauer, J.: Graph abstraction and abstract graph transformation. Technical report LNCS4549/TR-CTIT-07-50, July 2007Google Scholar
  6. 6.
    Corradini, A., Heindel, T., König, B., Nolte, D., Rensink, A.: Rewriting abstract structures: materialization explained categorically. In: Bojańczyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 169–188. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-17127-8_10CrossRefzbMATHGoogle Scholar
  7. 7.
    Dyck, J.: Increasing expressive power of graph rules and conditions and automatic verification with inductive invariants. Master’s thesis, University of Potsdam, Hasso Plattner Institute, Potsdam, Germany (2012)Google Scholar
  8. 8.
    Dyck, J.: Verification of graph transformation systems with k-inductive invariants. Ph.D. thesis, University of Potsdam, Hasso Plattner Institute, Potsdam, Germany (2020).  https://doi.org/10.25932/publishup-44274
  9. 9.
    Dyck, J., Giese, H.: Inductive invariant checking with partial negative application conditions. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 237–253. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21145-9_15CrossRefGoogle Scholar
  10. 10.
    Dyck, J., Giese, H.: k-inductive invariant checking for graph transformation systems. In: de Lara, J., Plump, D. (eds.) ICGT 2017. LNCS, vol. 10373, pp. 142–158. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-61470-0_9CrossRefzbMATHGoogle Scholar
  11. 11.
    Dyck, J., Giese, H.: k-inductive invariant checking for graph transformation systems. Technical report 119, Hasso Plattner Institute at the University of Potsdam, Potsdam, Germany (2017)Google Scholar
  12. 12.
    Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, Berlin (2006).  https://doi.org/10.1007/3-540-31188-2CrossRefzbMATHGoogle Scholar
  13. 13.
    Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: \(\cal{M}\)-adhesive transformation systems with nested application conditions. part 1: parallelism, concurrency and amalgamation. Math. Struct. Comput. Sci. 24(4) (2014).  https://doi.org/10.1017/S0960129512000357
  14. 14.
    Habel, A., Pennemann, K.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(2), 245–296 (2009).  https://doi.org/10.1017/S0960129508007202
  15. 15.
    Kulcsár, G.: A compass to controlled graph rewriting. Ph.D. thesis, Technische Universität Darmstadt, January 2019. http://tuprints.ulb.tu-darmstadt.de/9304/
  16. 16.
    Maximova, M., Giese, H., Krause, C.: Probabilistic timed graph transformation systems. J. Log. Algebr. Meth. Program. 101, 110–131 (2018).  https://doi.org/10.1016/j.jlamp.2018.09.003MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Microsoft Corporation: Z3. https://github.com/Z3Prover/z3
  18. 18.
    Orejas, F.: Attributed graph constraints. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 274–288. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-87405-8_19CrossRefzbMATHGoogle Scholar
  19. 19.
    Orejas, F.: Symbolic graphs for attributed graph constraints. J. Symb. Comput. 46(3), 294–315 (2011).  https://doi.org/10.1016/j.jsc.2010.09.009MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Orejas, F., Lambers, L.: Delaying constraint solving in symbolic graph transformation. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 43–58. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15928-2_4CrossRefzbMATHGoogle Scholar
  21. 21.
    Orejas, F., Lambers, L.: Symbolic attributed graphs for attributed graph transformation. ECEASST 30 (2010). http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/405
  22. 22.
    Orejas, F., Lambers, L.: Lazy graph transformation. Fundam. Inform. 118(1–2), 65–96 (2012).  https://doi.org/10.3233/FI-2012-706MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Pennemann, K.: Development of correct graph transformation systems. Ph.D. thesis, University of Oldenburg, Germany (2009). http://oops.uni-oldenburg.de/884/. URN http://nbn-resolving.de/urn:nbn:de:gbv:715-oops-9483
  24. 24.
    Poskitt, C.M., Plump, D.: Verifying monadic second-order properties of graph programs. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 33–48. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-09108-2_3CrossRefzbMATHGoogle Scholar
  25. 25.
    Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401–415. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24725-8_28CrossRefGoogle Scholar
  26. 26.
    Schneider, S., Lambers, L., Orejas, F.: Automated reasoning for attributed graph properties. STTT 20(6), 705–737 (2018).  https://doi.org/10.1007/s10009-018-0496-3CrossRefGoogle Scholar
  27. 27.
    Steenken, D.: Verification of infinite-state graph transformation systems via abstraction. Ph.D. thesis, University of Paderborn (2015). https://nbn-resolving.de/urn:nbn:de:hbz:466:2--15768
  28. 28.
    Steenken, D., Wehrheim, H., Wonisch, D.: Sound and complete abstract graph transformation. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 92–107. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-25032-3_7CrossRefzbMATHGoogle Scholar
  29. 29.
    Wang, X., Büttner, F., Lamo, Y.: Verification of graph-based model transformations using alloy. ECEASST 67 (2014).  https://doi.org/10.14279/tuj.eceasst.67.943

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.University of Potsdam, Hasso Plattner InstitutePotsdamGermany

Personalised recommendations