{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T00:47:28Z","timestamp":1767142048282,"version":"build-2238731810"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,5,9]],"date-time":"2015-05-09T00:00:00Z","timestamp":1431129600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s11704-015-4290-4","type":"journal-article","created":{"date-parts":[[2015,5,8]],"date-time":"2015-05-08T03:16:43Z","timestamp":1431055003000},"page":"364-374","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying specifications with associated attributes in graph transformation systems"],"prefix":"10.1007","volume":"9","author":[{"given":"Yu","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yankai","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ou","family":"Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiqiu","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,9]]},"reference":[{"key":"4290_CR1","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1007\/3-540-45832-8_30","volume":"2505","author":"L Baresi","year":"2002","unstructured":"Baresi L, Heckel R. Tutorial introduction to graph transformation: a software engineering perspective. Lecture Notes in Computer Science, 2002, 2505: 402\u2013429","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR2","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1016\/j.tcs.2012.01.032","volume":"424","author":"U Golas","year":"2012","unstructured":"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\u201368","journal-title":"Theoretical Computer Science"},{"key":"4290_CR3","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/BFb0053588","volume":"1382","author":"R Heckel","year":"1998","unstructured":"Heckel R. Compositional verification of reactive systems specified by graph transformation. Lecture Notes in Computer Science, 1998, 1382: 138\u2013153","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR4","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/978-3-540-30203-2_17","volume":"3256","author":"A Rensink","year":"2004","unstructured":"Rensink A, Schmidt A, Varr\u00f3 D. Model checking graph transformations: a comparison of two approaches. Lecture Notes in Computer Science, 2004, 3256: 226\u2013241","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR5","first-page":"411","volume-title":"Proceedings of the 1999 International Conference on Software Engineering","author":"M B Dwyer","year":"1999","unstructured":"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\u2013420"},{"issue":"1","key":"4290_CR6","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/s10009-011-0186-x","volume":"14","author":"A H Ghamarian","year":"2012","unstructured":"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\u201340","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"4290_CR7","first-page":"181","volume-title":"Proceedings of the Fundamentals of Algebraic Graph Transformation","author":"H Ehrig","year":"2006","unstructured":"Ehrig H, Ehrig K, Prange U, Taentzer G. Typed attributed graph transformation systems. In: Proceedings of the Fundamentals of Algebraic Graph Transformation. 2006, 181\u2013205"},{"key":"4290_CR8","first-page":"92","volume-title":"Lecture Notes in Computer Science","author":"A Schmidt","year":"2003","unstructured":"Schmidt A, Varr\u00f3 D. Checkvml: a tool for model checking visual modeling languages. Lecture Notes in Computer Science, 2003, 92\u201395"},{"key":"4290_CR9","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-642-00434-6_5","volume":"5452","author":"J E Rivera","year":"2009","unstructured":"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\u201373","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR10","first-page":"1","volume":"32","author":"A Rensink","year":"2011","unstructured":"Rensink A, Zambon E. Neighbourhood abstraction in groove. Electronic Communications of the EASST, 2011, 32: 1\u201313","journal-title":"Electronic Communications of the EASST"},{"key":"4290_CR11","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/978-3-540-68679-8_8","volume":"5065","author":"A Rensink","year":"2008","unstructured":"Rensink A. Explicit state model checking for graph grammars. Lecture Notes in Computer Science, 2008, 5065: 114\u2013132","journal-title":"Lecture Notes in Computer Science"},{"issue":"3","key":"4290_CR12","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1007\/s11704-013-2195-2","volume":"7","author":"S Konur","year":"2013","unstructured":"Konur S. A survey on temporal logics for specifying and verifying real-time systems. Frontiers of Computer Science in China, 2013, 7(3): 370\u2013403","journal-title":"Frontiers of Computer Science in China"},{"key":"4290_CR13","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/11817949_8","volume":"4137","author":"A Rensink","year":"2006","unstructured":"Rensink A. Model checking quantified computation tree logic. Lecture Notes in Computer Science, 2006, 4137: 110\u2013125","journal-title":"Lecture Notes in Computer Science"},{"issue":"3","key":"4290_CR14","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/1132960.1132962","volume":"38","author":"A Miller","year":"2006","unstructured":"Miller A, Donaldson A, Calder M. Symmetry in temporal logic model checking. ACM Computing Surveys (CSUR), 2006, 38(3): 8","journal-title":"ACM Computing Surveys (CSUR)"},{"issue":"1","key":"4290_CR15","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/s11704-010-0358-y","volume":"5","author":"C H Zhou","year":"2011","unstructured":"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\u201325","journal-title":"Frontiers of Computer Science in China"},{"issue":"7","key":"4290_CR16","doi-asserted-by":"crossref","first-page":"869","DOI":"10.1016\/j.ic.2008.04.002","volume":"206","author":"P Baldan","year":"2008","unstructured":"Baldan P, Corradini A, K\u00f6nig B. A framework for the verification of infinite-state graph transformation systems. Information and Computation, 2008, 206(7): 869\u2013907","journal-title":"Information and Computation"},{"issue":"1","key":"4290_CR17","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2008.04.071","volume":"213","author":"L Baresi","year":"2008","unstructured":"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\u201321","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"4290_CR18","first-page":"150","volume-title":"Proceedings of Workshop on Automated Verification of Critical Systems (AVoCS)","author":"A Rensink","year":"2003","unstructured":"Rensink A. Towards model checking graph grammars. In: Proceedings of Workshop on Automated Verification of Critical Systems (AVoCS). 2003, 150\u2013160"},{"key":"4290_CR19","unstructured":"Ben-Ari M. Principles of the spin model checker. Springer Heidelberg, 2008, volume 232"},{"key":"4290_CR20","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/j.entcs.2004.02.062","volume":"109","author":"S Gyapay","year":"2004","unstructured":"Gyapay S, Schmidt A, Varr\u00f3 D. Joint optimization and reachability analysis in graph transformation systems with time. Electronic Notes in Theoretical Computer Science, 2004, 109: 137\u2013147","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"4290_CR21","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-540-39958-2_18","volume":"2884","author":"F L Dotti","year":"2003","unstructured":"Dotti F L, Foss L, Ribeiro L, Santos O M. Verification of distributed object-based systems. Lecture Notes in Computer Science, 2003, 2884: 261\u2013275","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR22","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/j.entcs.2008.04.042","volume":"211","author":"B K\u00f6nig","year":"2008","unstructured":"K\u00f6nig 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\u2013210","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"4290_CR23","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/3-540-44685-0_26","volume":"2154","author":"P Baldan","year":"2001","unstructured":"Baldan P, Corradini A, K\u00f6nig B. A static analysis technique for graph transformation systems. Lecture Notes in Computer Science, 2001, 2154: 381\u2013395","journal-title":"Lecture Notes in Computer Science"},{"issue":"3","key":"4290_CR24","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/s10009-004-0155-8","volume":"6","author":"S Burmester","year":"2004","unstructured":"Burmester S, Giese H, Niere J, Tichy M, Wadsack J P, Wagner R, Wendehals L, Z\u00fcndorf A. Tool integration at the meta-model level: the fujaba approach. International Journal on Software Tools for Technology Transfer, 2004, 6(3): 203\u2013218","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"4290_CR25","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/11841883_22","volume":"4178","author":"L Baresi","year":"2006","unstructured":"Baresi L, Spoletini P. On the use of alloy to analyze graph transformation systems. Lecture Notes in Computer Science, 2006, 4178: 306\u2013320","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR26","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/11691617_19","volume":"3925","author":"H Kastenberg","year":"2006","unstructured":"Kastenberg H, Rensink A. Model checking dynamic states in groove. Lecture Notes in Computer Science, 2006, 3925: 299\u2013305","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR27","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1007\/978-3-540-25959-6_35","volume":"3062","author":"G Taentzer","year":"2004","unstructured":"Taentzer G. Agg: a graph transformation environment for modeling and validation of software. Lecture Notes in Computer Science, 2004, 3062: 446\u2013453","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR28","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-642-03764-1_6","volume":"5560","author":"J Whittle","year":"2009","unstructured":"Whittle J, Jayaraman P, Elkhodary A, Moreira A, Ara\u00fajo J.Mata: a unified approach for composing uml aspect models based on graph transformation. Lecture Notes in Computer Science, 2009, 5560: 191\u2013237","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR29","first-page":"105","volume-title":"In Proceedings of the 24thInternational Conference on Software Engineering","author":"J H Hausmann","year":"2002","unstructured":"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 24thInternational Conference on Software Engineering. 2002, 105\u2013115"},{"issue":"4","key":"4290_CR30","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1016\/j.scico.2010.02.006","volume":"77","author":"S A Costa","year":"2012","unstructured":"Costa S A, Ribeiro L. Verification of graph grammars using a logical approach. Science of Computer Programming, 2012, 77(4): 480\u2013504","journal-title":"Science of Computer Programming"},{"issue":"4","key":"4290_CR31","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1049\/iet-sen.2008.0059","volume":"3","author":"V Rafe","year":"2009","unstructured":"Rafe V, Rahmani A T, Baresi L, Spoletini P. Towards automated verification of layered graph transformation specifications. IET Software, 2009, 3(4): 276\u2013291","journal-title":"IET Software"},{"key":"4290_CR32","first-page":"41","volume-title":"Electronic Communications of the EASST","author":"A Vandin","year":"2011","unstructured":"Vandin A, Lafuente A L. Towards a maude tool for model checking temporal graph properties. Electronic Communications of the EASST, 2011, 41"},{"key":"4290_CR33","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/11513988_15","volume":"3576","author":"M B Dwyer","year":"2005","unstructured":"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\u2013152","journal-title":"Lecture Notes in Computer Science"},{"key":"4290_CR34","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1007\/978-3-642-15928-2_19","volume":"6372","author":"F Gadducci","year":"2012","unstructured":"Gadducci F, Lafuente A L, Vandin A. Counterpart semantics for a second-order \u00b5-calculus. Lecture Notes in Computer Science, 2012, 6372: 282\u2013297","journal-title":"Lecture Notes in Computer Science"},{"issue":"2","key":"4290_CR35","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1109\/TSE.2010.39","volume":"37","author":"L Baresi","year":"2011","unstructured":"Baresi L, Ghezzi C, Mottola L. Loupe: verifying publish-subscribe architectures with a magnifying lens. IEEE Transactions on Software Engineering, 2011, 37(2): 228\u2013246","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-015-4290-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-015-4290-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-015-4290-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T17:01:22Z","timestamp":1559408482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-015-4290-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,9]]},"references-count":35,"aliases":["10.1007\/s11704-014-4290-4"],"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["4290"],"URL":"https:\/\/doi.org\/10.1007\/s11704-015-4290-4","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,9]]}}}