|
|
Verifying specifications with associated attributes in graph transformation systems |
Yu ZHOU1,2,*( ),Yankai HUANG1,Ou WEI1,Zhiqiu HUANG1 |
1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China 2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China |
|
|
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
|
Corresponding Author(s):
Yu ZHOU
|
Issue Date: 18 May 2015
|
|
1 |
Baresi L, Heckel R. Tutorial introduction to graph transformation: a software engineering perspective. Lecture Notes in Computer Science, 2002, 2505: 402-429
https://doi.org/10.1007/3-540-45832-8_30
|
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
https://doi.org/10.1016/j.tcs.2012.01.032
|
3 |
Heckel R. Compositional verification of reactive systems specified by graph transformation. Lecture Notes in Computer Science, 1998, 1382: 138-153
https://doi.org/10.1007/BFb0053588
|
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
https://doi.org/10.1007/978-3-540-30203-2_17
|
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
https://doi.org/10.1145/302405.302672
|
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
https://doi.org/10.1007/s10009-011-0186-x
|
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
https://doi.org/10.1007/978-3-540-45221-8_8
|
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
https://doi.org/10.1007/978-3-642-00434-6_5
|
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
https://doi.org/10.1007/978-3-540-68679-8_8
|
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
https://doi.org/10.1007/s11704-013-2195-2
|
13 |
Rensink A. Model checking quantified computation tree logic. Lecture Notes in Computer Science, 2006, 4137: 110-125
https://doi.org/10.1007/11817949_8
|
14 |
Miller A, Donaldson A, Calder M. Symmetry in temporal logic model checking. ACM Computing Surveys (CSUR), 2006, 38(3): 8
https://doi.org/10.1145/1132960.1132962
|
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
https://doi.org/10.1007/s11704-010-0358-y
|
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
https://doi.org/10.1016/j.ic.2008.04.002
|
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
https://doi.org/10.1016/j.entcs.2008.04.071
|
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
https://doi.org/10.1016/j.entcs.2004.02.062
|
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
https://doi.org/10.1007/978-3-540-39958-2_18
|
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
https://doi.org/10.1016/j.entcs.2008.04.042
|
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
https://doi.org/10.1007/3-540-44685-0_26
|
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
https://doi.org/10.1007/s10009-004-0155-8
|
25 |
Baresi L, Spoletini P. On the use of alloy to analyze graph transformation systems. Lecture Notes in Computer Science, 2006, 4178: 306-320
https://doi.org/10.1007/11841883_22
|
26 |
Kastenberg H, Rensink A. Model checking dynamic states in groove. Lecture Notes in Computer Science, 2006, 3925: 299-305
https://doi.org/10.1007/11691617_19
|
27 |
Taentzer G. Agg: a graph transformation environment for modeling and validation of software. Lecture Notes in Computer Science, 2004, 3062: 446-453
https://doi.org/10.1007/978-3-540-25959-6_35
|
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
https://doi.org/10.1007/978-3-642-03764-1_6
|
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
https://doi.org/10.1145/581352.581355
|
30 |
Costa S A, Ribeiro L. Verification of graph grammars using a logical approach. Science of Computer Programming, 2012, 77(4): 480-504
https://doi.org/10.1016/j.scico.2010.02.006
|
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
https://doi.org/10.1049/iet-sen.2008.0059
|
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
https://doi.org/10.1007/11513988_15
|
34 |
Gadducci F, Lafuente A L, Vandin A. Counterpart semantics for a second-order μ-calculus. Lecture Notes in Computer Science, 2012, 6372: 282-297
https://doi.org/10.1007/978-3-642-15928-2_19
|
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
https://doi.org/10.1109/TSE.2010.39
|
[1] |
Supplementary Material-Highlights in 3-page ppt
|
Download
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|