Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front. Comput. Sci.    2015, Vol. 9 Issue (3) : 364-374    https://doi.org/10.1007/s11704-015-4290-4
RESEARCH ARTICLE
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
 Download: PDF(506 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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
 Cite this article:   
Yu ZHOU,Yankai HUANG,Ou WEI, et al. Verifying specifications with associated attributes in graph transformation systems[J]. Front. Comput. Sci., 2015, 9(3): 364-374.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-015-4290-4
https://academic.hep.com.cn/fcs/EN/Y2015/V9/I3/364
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
[1] Daian YUE, Vania JOLOBOFF, Frédéric MALLET. TRAP: trace runtime analysis of properties[J]. Front. Comput. Sci., 2020, 14(3): 143201-.
[2] Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[3] Tun LI, Jun YE, Qingping TAN. Towards functional verifying a family of SystemC TLMs[J]. Front. Comput. Sci., 2020, 14(1): 53-66.
[4] Abdelkrim CHEBIEB, Yamine AIT AMEUR. A formal model for plastic human computer interfaces[J]. Front. Comput. Sci., 2018, 12(2): 351-375.
[5] Yongwang ZHAO, Zhibin YANG, Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.
[6] Ruifeng XU,Lin GUI,Qin LU,Shuai WANG,Jian XU. Incorporating multi-kernel function and Internet verification for Chinese person name disambiguation[J]. Front. Comput. Sci., 2016, 10(6): 1026-1038.
[7] Jiankun HE,Xishun ZHAO. Reasoning about actions with loops via Hoare logic[J]. Front. Comput. Sci., 2016, 10(5): 870-888.
[8] Xuzhou LI,Yilong YIN,Yanbin NING,Gongping YANG,Lei PAN. A hybrid biometric identification framework for high security applications[J]. Front. Comput. Sci., 2015, 9(3): 392-401.
[9] Fei HE,Xiaoyu SONG,Ming GU,Jiaguang SUN. Generalized interface automata with multicast synchronization[J]. Front. Comput. Sci., 2015, 9(1): 1-14.
[10] Xiaoxiao YANG,Yu ZHANG,Ming FU,Xinyu FENG. A temporal programming model with atomic blocks based on projection temporal logic[J]. Front. Comput. Sci., 2014, 8(6): 958-976.
[11] Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[12] Jean-Vivien MILLO, Frédéric MALLET, Anthony COADOU, S RAMESH. Scenario-based verification in presence of variability using a synchronous approach[J]. Front Comput Sci, 2013, 7(5): 650-672.
[13] Van Chan NGO, Jean-Pierre TALPIN, Thierry GAUTIER, Paul Le GUERNIC, Lo?c BESNARD. Formal verification of synchronous data-flow program transformations toward certified compilers[J]. Front Comput Sci, 2013, 7(5): 598-616.
[14] Zhiyuan LIU, Jun PANG, Chenyi ZHANG. Design and formal verification of a CEM protocol with transparent TTP[J]. Front Comput Sci, 2013, 7(2): 279-297.
[15] Yuehua DAI, Yi SHI, Yong QI, Jianbao REN, Peijian WANG. Design and verification of a lightweight reliable virtual machine monitor for a many-core architecture[J]. Front Comput Sci, 2013, 7(1): 34-43.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed