Model Checking Graph Transformations: A Comparison of Two Approaches

13 years 10 months ago

Download wwwhome.cs.utwente.nl

Model checking is increasingly popular for hardware and, more recently, software veriﬁcation. In this paper we describe two different approaches to extend the beneﬁts of model checking to systems whose behavior is speciﬁed by graph transformation systems. One approach is to encode the graphs into the ﬁxed state vectors and the transformation rules into guarded commands that modify these state vectors appropriately to enjoy all the beneﬁts of the years of experience incorporated in existing model checking tools. The other approach is to simulate the graph production rules directly and build the state space directly from the resultant graphs and derivations. This avoids the preprocessing nd makes additional abstraction techniques available to handle symmetries and dynamic allocation. In this paper we compare these approaches on the basis of three case studies elaborated in both of them, and we evaluate the results. Our conclusion is that the ﬁrst approach outperforms the seco...

Arend Rensink, Ákos Schmidt, Dániel

Real-time Traffic