{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T10:40:34Z","timestamp":1736419234178,"version":"3.32.0"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,6,13]],"date-time":"2006-06-13T00:00:00Z","timestamp":1150156800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2006,9]]},"DOI":"10.1007\/s10270-006-0014-z","type":"journal-article","created":{"date-parts":[[2006,6,12]],"date-time":"2006-06-12T13:55:14Z","timestamp":1150120514000},"page":"289-311","source":"Crossref","is-referenced-by-count":5,"title":["Verifying Object-based Graph Grammars"],"prefix":"10.1007","volume":"5","author":[{"given":"Fernando Lu\u00eds","family":"Dotti","sequence":"first","affiliation":[]},{"given":"Leila","family":"Ribeiro","sequence":"additional","affiliation":[]},{"given":"Osmar Marchi dos","family":"Santos","sequence":"additional","affiliation":[]},{"given":"F\u00e1bio","family":"Pasini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,13]]},"reference":[{"issue":"8","key":"14_CR1","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1109\/32.707696","volume":"24","author":"G.S. Avrunin","year":"1998","unstructured":"Avrunin G.S., Corbett J.C., Dillon L.K. (1998). Analyzing partially-implemented real-time systems. IEEE Trans. Softw. Eng. 24(8):602\u2013614","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B.: Verifying finite-state graph grammars: an unfolding-based approach. In: 15th International conference on concurrency theory, Vol. 3170 of LNCS, UK, pp. 83\u201398. Springer, Berlin Heidelberg New York (2004)","DOI":"10.1007\/978-3-540-28644-8_6"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Baldan, P., K\u00f6nig, B.: Approximating the behaviour of graph transformation systems. In: 1st International conference on graph transformation, vol 2505 of LNCS, Spain, pp. 14\u201329. Springer, Berlin Heidelberg New York (2002)","DOI":"10.1007\/3-540-45832-8_4"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Sinha, N., Thati, P.: Automated assume-guarantee reasoning for simulation conformance. In: 17th International conference on computer aided verification, vol 3576 of LNCS, UK, pp. 534\u2013547. Springer, Berlin Heidelberg New York (2005)","DOI":"10.1007\/11513988_51"},{"key":"14_CR5","unstructured":"Chamillard, A.: An empirical comparison of static concurrency analysis techniques. PhD Thesis, University of Massachusetts at Amherst, 1996"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Chechik, M., P\u0103un, D.O.: Events in property patterns. In: 5th and 6th SPIN workshops, vol 1680 of LNCS, Germany, pp. 154\u2013167. Springer, Berlin Heidelberg New York (1999)","DOI":"10.1007\/3-540-48234-2_13"},{"issue":"1","key":"14_CR7","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/295558.295570","volume":"8","author":"S.C. Cheung","year":"1999","unstructured":"Cheung S.C., Kramer J. (1999). Checking safety properties using compositional reachability analysis. ACM Trans. Softw. Eng. Methodol. 8(1):49\u201378","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"14_CR8","unstructured":"Cho, S.M., et\u00a0al.: Applying Model checking to Concurrent Object-Oriented Software. In: 4th International Symposium on Autonomous Decentralized Systems, Japan, pp. 380\u2013383. IEEE CS Press, Calgary (1999)"},{"issue":"5","key":"14_CR9","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1145\/277652.277754","volume":"33","author":"C. Colby","year":"1998","unstructured":"Colby C., Godefroid P., Jagadeesan L.J. (1998). Automatically closing open reactive programs. ACM SIGPLAN Notices 33(5):345\u2013357","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Copstein, B., M\u00f3ra, M.C., Ribeiro, L.: An environment for formal modeling and simulation of control systems. In: 33rd Annual simulation symposium, USA, pp. 74\u201382. IEEE CS Press, Calgary (2000)","DOI":"10.1109\/SIMSYM.2000.844903"},{"key":"14_CR11","unstructured":"Copstein, B., Ribeiro, L.: Specifying simulation models using graph grammars. In: 10th European simulation symposium, UK, pp. 60\u201364. SCS, (1998)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., et\u00a0al.: Bandera: extracting finite-state models from Java source code. In: 22nd International Conference on Software Engineering, Ireland, pp. 439\u2013448. ACM Press, New York (2000)","DOI":"10.1145\/337180.337234"},{"key":"14_CR13","unstructured":"Demartini, C., Iosif, R., Sisto, R.: Modeling and validation of Java multithreading applications using SPIN. In: Najm, E., Holzmann, G., Serhrouchni, A., (eds.) 4th SPIN Workshop, France (1998)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Demartini, C., Iosif, R., Sisto, R.: dSPIN: A dynamic extension of SPIN. In: 6th SPIN Workshop, vol 1680 of LNCS, France, pp. 261\u2013276. Springer, Berlin Heidelberg New York (1999)","DOI":"10.1007\/3-540-48234-2_20"},{"key":"14_CR15","unstructured":"Dotti, F.L., Duarte, L.M., Copstein, B., Ribeiro, L.: Simulation of mobile applications. In: 2002 Communication Networks and Distributed Systems Modeling and Simulation Conference, pp. 261\u2013267. SCS, (2002)"},{"key":"14_CR16","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2004.12.026","volume":"127-1","author":"F.L. Dotti","year":"2005","unstructured":"Dotti F.L., Duarte L.M., Foss L., Ribeiro L., Russi D., Santos O.M. (2005). An environment for the development of concurrent object-based applications. Electron. Notes Theor. Comput. Sci. 127-1:3\u201313","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"14_CR17","unstructured":"Dotti, F.L., Foss, L., Ribeiro, L., Santos, O.M.: Formal specification and verification of distributed systems (in portuguese). In: 17th Brazilian Symposium on Software Engineering, Brazil, pp. 225\u2013240. SBC, (2003)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Dotti, F.L., Foss, L., Ribeiro, L., Santos, O.M.: Verification of object-based distributed systems. In: 6th International Conference on Formal Methods for Open Object-Based Distributed Systems, vol 2884 of LNCS, France, pp. 261\u2013275. Springer, Berlin berlin Heidelberg New York (2003)","DOI":"10.1007\/978-3-540-39958-2_18"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Dotti, F.L., Ribeiro, L.: Specification of mobile code systems using graph grammars. In: Smith S.F., Talcott, C.L., (eds.) Formal Methods for Open Object-Based Distributed Systems IV, IFIF TC6\/WG6.1 Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000), September 6\u20138, 2000, Stanford, California, USA, vol 177 of IFIP Conference Proceedings, pp. 45\u201364. Kluwer, Dordrecht (2000)","DOI":"10.1007\/978-0-387-35520-7_3"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Dotti, F.L., Ribeiro, L., Santos, O.M.: Specification and analysis of fault behaviours using graph grammars. In: 2nd International Workshop on Applications of Graph Transformation with Industrial Relevance, vol 3062 of LNCS, USA, pp. 120\u2013133. Springer, Berlin Heidelberg New York (2003)","DOI":"10.1007\/978-3-540-25959-6_9"},{"key":"14_CR21","unstructured":"Duarte, L., Dotti, F.L.: Development of an active network architecture using mobile agents \u2013 a case study. Technical Report TR-043, FACIN \u2013 PPGCC \u2013 PUCRS, (2004)"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: 2nd Workshop on Formal Methods in Software Practice, USA, pp. 7\u201315. ACM Press, New York (1998)","DOI":"10.1145\/298595.298598"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 21st International Conference on Software Engineering, USA, pp. 411\u2013420. IEEE CS Press, Calgary (1999)","DOI":"10.1145\/302405.302672"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., P\u0103s\u0103reanu, C.S.: Filter-based model checking of partial systems. In: 6th International Symposium on Foundations of Software Engineering, USA, pp. 189\u2013202. ACM Press, New York (1998)","DOI":"10.1145\/288195.288307"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., P\u0103s\u0103reanu, C.S.: Model checking generic container implementations. In: International Seminar on Generic Programming, vol 1766 of LNCS, UK, pp. 162\u2013177. Springer, Berlin Heidelberg New York (2000)","DOI":"10.1007\/3-540-39953-4_13"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Barringer, H.: Assumption generation for software component verification. In: 17th IEEE International Conference on Automated Software Engineering, UK, pp. 3\u201312. IEEE CS Press, (2002)","DOI":"10.1109\/ASE.2002.1114984"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: 24th Symposium on Principles of Programming Languages, France, pp. 174\u2013186. ACM Press, New York (1997)","DOI":"10.1145\/263699.263717"},{"issue":"2","key":"14_CR28","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1109\/MS.1985.230351","volume":"2","author":"D. Helmbold","year":"1985","unstructured":"Helmbold D., Luckham D. (1985). Debugging ada tasking programs. IEEE Softw. 2(2):47\u201357","journal-title":"IEEE Softw."},{"key":"14_CR29","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare C.A.R. (1985). Communicating Sequential Processes. Prentice Hall, USA"},{"issue":"5","key":"14_CR30","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann G.J. (1997). The model checker SPIN. IEEE Trans. Softw. Eng. 23(5):279\u2013295","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"14_CR31","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1006\/inco.2000.2893","volume":"164","author":"O. Kupferman","year":"2001","unstructured":"Kupferman O., Vardi M.Y., Wolper P. (2001). Module checking. Inf. Comput. 164(1):322\u2013344","journal-title":"Inf. Comput."},{"issue":"3","key":"14_CR32","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport L. (1994). The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3):872\u2013923","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Leue, S., Holzmann, G.: v-Promela: a visual, object oriented language for SPIN. In: 2nd International Symposium on Object-Oriented Real-Time Distributed Computing, France, pp. 14\u201323. IEEE CS Press, Calgary (1999)","DOI":"10.1109\/ISORC.1999.776345"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Lilius, J., Paltor, I.P.: vUML: a tool for verifying UML models. In: 14th International Conference on Automated Software Engineering, USA, pp. 255\u2013258. IEEE CS Press, Calgary (1999)","DOI":"10.1109\/ASE.1999.802301"},{"issue":"3","key":"14_CR35","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Lynch N., Tuttle M. (1989). An introduction to input\/output automata. CWI-Q. 2(3):219\u2013246","journal-title":"CWI-Q."},{"key":"14_CR36","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Manna Z., Pnueli A. (1991). The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin Heidelberg New York"},{"key":"14_CR37","unstructured":"Mehlitz, P.C., Visser, W., Penix, J.: The JPF runtime verification system. Manual for the JPF tool (2005)"},{"key":"14_CR38","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner R. (1989). Communication and Concurrency. Prentice Hall, London"},{"key":"14_CR39","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of software: a comparative case study. In: Theoretical and Practical Aspects of SPIN Model Checking, vol 1680 of LNCS, UK, pp. 168\u2013183. Springer, Berlin Heidelberg New York (1999)","DOI":"10.1007\/3-540-48234-2_14"},{"key":"14_CR40","unstructured":"Petri, CA.: Kommunikation mit Automaten. PhD Thesis, Schriften des Institutes f\u00fcr Instrumentelle Mathematik, Universit\u00e4t Bonn (1962)"},{"key":"14_CR41","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models for Concurrent Systems, NATO ASI F13, pp. 123\u2013144. Springer, Berlin Heidelberg New York (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"14_CR42","unstructured":"Wolfgang Reisig. Petri Nets, volume 4 of EATCS Monographs on Theoretical Computer Science. Springer, Berlin Heidelberg New York (1985)"},{"key":"14_CR43","doi-asserted-by":"crossref","unstructured":"Rensink, A., Schmidt, \u00c1., Varr\u00f3, D.: Model checking graph transformations: a comparison of two approaches. In: 2nd International Conference on Graph Transformation, vol 3256 of LNCS, Italy, pp. 226\u2013241. Springer, Berlin Heidelberg New York (2004)","DOI":"10.1007\/978-3-540-30203-2_17"},{"volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation, vol 1: Foundations","year":"1997","key":"14_CR44","unstructured":"Rozenberg G. (eds) (1997). Handbook of Graph Grammars and Computing by Graph Transformation, vol 1: Foundations. World Scientific Publisher, Cleveland"},{"key":"14_CR45","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.entcs.2004.02.061","volume":"109","author":"O.M. Santos","year":"2004","unstructured":"Santos O.M., Dotti F.L., Ribeiro L. (2004). Verifying object-based graph grammars. Eletron. Notes. Theor. Compu. Sci. 109:125\u2013136","journal-title":"Eletron. Notes. Theor. Compu. Sci."},{"issue":"3","key":"14_CR46","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip F. (1995). A survey of program slicing techniques. J. Program. Lang. 3(3):121\u2013189","journal-title":"J. Program. Lang."},{"key":"14_CR47","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Branching vs linear time: final showdown. In: 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol 2031 of LNCS, Italy, pp. 1\u201322, Springer, Berlin Heidelberg New York (2001)","DOI":"10.1007\/3-540-45319-9_1"},{"issue":"2","key":"14_CR48","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s10270-003-0050-x","volume":"3","author":"D. Varr\u00f3","year":"2004","unstructured":"Varr\u00f3 D. (2004). Automated formal verification of visual modeling languages by model checking. Softw. Syst. Model. 3(2):85\u2013113","journal-title":"Softw. Syst. Model."},{"key":"14_CR49","unstructured":"Vaught, A.: Graphing with Gnuplot and Xmgr: two graphing packages available under linux. Linux J. 28(7), (1996)."},{"key":"14_CR50","doi-asserted-by":"crossref","unstructured":"Winter, K., Duke, R.: Model checking Object-Z using ASM. In: 3rd International Conference on Integrated Formal Methods, vol 2335 of LNCS, Finland, pp. 165\u2013184. Springer, Berlin Heidelberg New York (2002)","DOI":"10.1007\/3-540-47884-1_10"},{"key":"14_CR51","doi-asserted-by":"crossref","unstructured":"Xie, F., Browne, J.C.: Verified systems by composition from verified components. In: 10th International Symposium on Foundations of Software Engineering, Finland, pp. 277\u2013286. ACM Press, New York (2003)","DOI":"10.1145\/940071.940109"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-006-0014-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-006-0014-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-006-0014-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T09:58:21Z","timestamp":1736416701000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-006-0014-z"}},"subtitle":["An Assume-guarantee Approach"],"short-title":[],"issued":{"date-parts":[[2006,6,13]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,9]]}},"alternative-id":["14"],"URL":"https:\/\/doi.org\/10.1007\/s10270-006-0014-z","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2006,6,13]]}}}