Verifying specifications with associated attributes in graph transformation systems

Abstract

Graph transformation is an important modeling and analysis technique widely applied in software engineering. The attributes can naturally conceptualize the properties of the modeled artifacts. However, the lack of support for the specification of such attribute correspondence by ordinary propositional temporal logics hampers its further application during verification. Different from the theoretical investigations on quantified second order logics, we propose a practical and light-weight approach for the verification of this kind of temporal specifications with associated attributes. Particularly, we apply our approach and extend the generalpurpose graph transformation modeling tool: Groove. Moreover, symmetry reduction techniques are exploited to reduce the number of states. Experiments with performance evaluations complement our discussion and demonstrate the feasibility and efficiency of our approach.

Keywords

graph grammar / software design / verification

References

[1] Baresi L, Heckel R. Tutorial introduction to graph transformation: a software engineering perspective. Lecture Notes in Computer Science, 2002, 2505: 402-429

[2] Golas U, Lambers L, Ehrig H, Orejas F. Attributed graph transformation with inheritance: efficient conflict detection and local confluence analysis using abstract critical pairs. Theoretical Computer Science, 2012, 424: 46-68

[3] Heckel R. Compositional verification of reactive systems specified by graph transformation. Lecture Notes in Computer Science, 1998, 1382: 138-153

[4] Rensink A, Schmidt A, Varró D. Model checking graph transformations: a comparison of two approaches. Lecture Notes in Computer Science, 2004, 3256: 226-241

[5] Dwyer M B, Avrunin G S, Corbett J C. Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering. 1999, 411-420

[6] Ghamarian A H, Mol M, Rensink A, Zambon E, Zimakova M. Modelling and analysis using groove. International Journal on Software Tools for Technology Transfer, 2012, 14(1): 15-40

[7] Ehrig H, Ehrig K, Prange U, Taentzer G. Typed attributed graph transformation systems. In: Proceedings of the Fundamentals of Algebraic Graph Transformation. 2006, 181-205

[8] Schmidt A, Varró D. Checkvml: a tool for model checking visual modeling languages. Lecture Notes in Computer Science, 2003, 92-95

[9] Rivera J E, Guerra E, Lara J, Vallecillo A. Analyzing rule-based behavioral semantics of visual modeling languages with maude. Lecture Notes in Computer Science, 2009, 5452: 54-73

[10] Rensink A, Zambon E. Neighbourhood abstraction in groove. Electronic Communications of the EASST, 2011, 32: 1-13

[11] Rensink A. Explicit state model checking for graph grammars. Lecture Notes in Computer Science, 2008, 5065: 114-132

[12] Konur S. A survey on temporal logics for specifying and verifying real-time systems. Frontiers of Computer Science in China, 2013, 7(3): 370-403

[13] Rensink A. Model checking quantified computation tree logic. Lecture Notes in Computer Science, 2006, 4137: 110-125

[14] Miller A, Donaldson A, Calder M. Symmetry in temporal logic model checking. ACM Computing Surveys (CSUR), 2006, 38(3): 8

[15] Zhou C H, Sun B, Liu Z F. Abstraction for model checking multi-agent systems. Frontiers of Computer Science in China, 2011, 5(1): 14-25

[16] Baldan P, Corradini A, König B. A framework for the verification of infinite-state graph transformation systems. Information and Computation, 2008, 206(7): 869-907

[17] Baresi L, Rafe V, Rahmani A T, Spoletini P. An efficient solution for model checking graph transformation systems. Electronic Notes in Theoretical Computer Science, 2008, 213(1): 3-21

[18] Rensink A. Towards model checking graph grammars. In: Proceedings of Workshop on Automated Verification of Critical Systems (AVoCS). 2003, 150-160

[19] Ben-Ari M. Principles of the spin model checker. Springer Heidelberg, 2008, volume 232

[20] Gyapay S, Schmidt A, Varró D. Joint optimization and reachability analysis in graph transformation systems with time. Electronic Notes in Theoretical Computer Science, 2004, 109: 137-147

[21] Dotti F L, Foss L, Ribeiro L, Santos O M. Verification of distributed object-based systems. Lecture Notes in Computer Science, 2003, 2884: 261-275

[22] König B, Kozioura V. Augur 2: a new version of a tool for the analysis of graph transformation systems. Electronic Notes in Theoretical Computer Science, 2008, 211: 201-210

[23] Baldan P, Corradini A, König B. A static analysis technique for graph transformation systems. Lecture Notes in Computer Science, 2001, 2154: 381-395

[24] Burmester S, Giese H, Niere J, Tichy M, Wadsack J P, Wagner R, Wendehals L, Zündorf A. Tool integration at the meta-model level: the fujaba approach. International Journal on Software Tools for Technology Transfer, 2004, 6(3): 203-218

[25] Baresi L, Spoletini P. On the use of alloy to analyze graph transformation systems. Lecture Notes in Computer Science, 2006, 4178: 306-320

[26] Kastenberg H, Rensink A. Model checking dynamic states in groove. Lecture Notes in Computer Science, 2006, 3925: 299-305

[27] Taentzer G. Agg: a graph transformation environment for modeling and validation of software. Lecture Notes in Computer Science, 2004, 3062: 446-453

[28] Whittle J, Jayaraman P, Elkhodary A, Moreira A, Araújo J. Mata: a unified approach for composing uml aspect models based on graph transformation. Lecture Notes in Computer Science, 2009, 5560: 191-237

[29] Hausmann J H, Heckel R, Taentzer G. Detection of conflicting functional requirements in a use case-driven approach: a static analysis technique based on graph transformation. In Proceedings of the 24th International Conference on Software Engineering. 2002, 105-115

[30] Costa S A, Ribeiro L. Verification of graph grammars using a logical approach. Science of Computer Programming, 2012, 77(4): 480-504

[31] Rafe V, Rahmani A T, Baresi L, Spoletini P. Towards automated verification of layered graph transformation specifications. IET Software, 2009, 3(4): 276-291

[32] Vandin A, Lafuente A L. Towards a maude tool for model checking temporal graph properties. Electronic Communications of the EASST, 2011, 41

[33] Dwyer M B, Hatcliff J, Hoosier M. Building your own software model checker using the bogor extensible model checking framework. Lecture Notes in Computer Science, 2005, 3576: 148-152

[34] Gadducci F, Lafuente A L, Vandin A. Counterpart semantics for a second-order μ-calculus. Lecture Notes in Computer Science, 2012, 6372: 282-297

[35] Baresi L, Ghezzi C, Mottola L. Loupe: verifying publish-subscribe architectures with a magnifying lens. IEEE Transactions on Software Engineering, 2011, 37(2): 228-246

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg