{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:45Z","timestamp":1750220685412,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319576657"},{"type":"electronic","value":"9783319576664"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57666-4_11","type":"book-chapter","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T12:18:42Z","timestamp":1491999522000},"page":"172-190","source":"Crossref","is-referenced-by-count":4,"title":["Reasoning About Connectors in Coq"],"prefix":"10.1007","author":[{"given":"Xiyue","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weijiang","family":"Hong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,13]]},"reference":[{"key":"11_CR1","unstructured":"Package of source files. https:\/\/github.com\/liyi-david\/reoincoq"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Arbab, F., Astefanoaei, L., de Boer, F.S., Sun, M., Rutten, J.: Fault-based test case generation for component connectors. In: Proceedings of TASE 2009, pp. 147\u2013154. IEEE Computer Society (2009)","DOI":"10.1109\/TASE.2009.14"},{"issue":"3","key":"11_CR3","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F Arbab","year":"2004","unstructured":"Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329\u2013366 (2004)","journal-title":"Math. Struct. Comput. Sci."},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-40020-2_2","volume-title":"Recent Trends in Algebraic Development Techniques","author":"F Arbab","year":"2003","unstructured":"Arbab, F., Rutten, J.J.M.M.: A coinductive calculus of component connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2002. LNCS, vol. 2755, pp. 34\u201355. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-40020-2_2"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-16561-0_15","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"C Baier","year":"2010","unstructured":"Baier, C., Blechmann, T., Klein, J., Kl\u00fcppelholz, S., Leister, W.: Design and verification of systems with exogenous coordination using vereofy. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 97\u2013111. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16561-0_15"},{"key":"11_CR6","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.scico.2005.10.008","volume":"61","author":"C Baier","year":"2006","unstructured":"Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61, 75\u2013113 (2006)","journal-title":"Sci. Comput. Program."},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/11925040_2","volume-title":"Leveraging Applications of Formal Methods","author":"D Clarke","year":"2006","unstructured":"Clarke, D., Costa, D., Arbab, F.: Modelling coordination in biological systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 9\u201325. Springer, Heidelberg (2006). doi: 10.1007\/11925040_2"},{"key":"11_CR8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W-P Roever de","year":"1998","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, New York (1998)"},{"key":"11_CR9","unstructured":"Huet, G., Kahn, G., Paulin-Mohring, C.: The coq proof assistant a tutorial. Rapport Technique, 178 (1997)"},{"key":"11_CR10","volume-title":"Systematic Software Development Using VDM","author":"CB Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall, Upper Saddle River (1990)"},{"issue":"1","key":"11_CR11","first-page":"201","volume":"22","author":"STQ Jongmans","year":"2012","unstructured":"Jongmans, S.T.Q., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comp. Sci. 22(1), 201\u2013251 (2012)","journal-title":"Sci. Ann. Comp. Sci."},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-68265-3_11","volume-title":"Coordination Models and Languages","author":"R Khosravi","year":"2008","unstructured":"Khosravi, R., Sirjani, M., Asoudeh, N., Sahebi, S., Iravanchi, H.: Modeling and analysis of Reo connectors using alloy. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 169\u2013183. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-68265-3_11"},{"issue":"9","key":"11_CR13","doi-asserted-by":"crossref","first-page":"688","DOI":"10.1016\/j.scico.2008.09.020","volume":"74","author":"S Kl\u00fcppelholz","year":"2009","unstructured":"Kl\u00fcppelholz, S., Baier, C.: Symbolic model checking for channel-based component connectors. Sci. Comput. Program. 74(9), 688\u2013701 (2009)","journal-title":"Sci. Comput. Program."},{"key":"11_CR14","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s00165-011-0191-6","volume":"24","author":"N Kokash","year":"2012","unstructured":"Kokash, N., Krause, C., de Vink, E.: Reo+mCRL2: a framework for model-checking dataflow in service compositions. Formal Aspects Comput. 24, 187\u2013216 (2012)","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"11_CR15","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1016\/j.scico.2015.10.016","volume":"113","author":"Y Li","year":"2015","unstructured":"Li, Y., Sun, M.: Modeling and verification of component connectors in Coq. Sci. Comput. Program. 113(3), 285\u2013301 (2015)","journal-title":"Sci. Comput. Program."},{"key":"11_CR16","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1998)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Sun, M.: Connectors as designs: the time dimension. In: Proceedings of TASE 2012, pp. 201\u2013208. IEEE Computer Society (2012)","DOI":"10.1109\/TASE.2012.36"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Sun, M., Arbab, F.: Web services choreography and orchestration in reo and constraint automata. In: Proceedings of SAC 2007, pp. 346\u2013353. ACM (2007)","DOI":"10.1145\/1244002.1244085"},{"issue":"7\u20138","key":"11_CR19","first-page":"799","volume":"77","author":"M Sun","year":"2012","unstructured":"Sun, M., Arbab, F., Aichernig, B.K., Astefanoaei, L., de Boer, F.S., Rutten, J.: Connectors as designs: modeling, refinement and test case generation. Sci. Comput. Program. 77(7\u20138), 799\u2013822 (2012)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57666-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:04:42Z","timestamp":1750197882000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57666-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319576657","9783319576664"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57666-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}