{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:49:55Z","timestamp":1778914195957,"version":"3.51.4"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,6,1]],"date-time":"2012-06-01T00:00:00Z","timestamp":1338508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004965","name":"Sixth Framework Programme","doi-asserted-by":"publisher","award":["IST-2005-016004"],"award-info":[{"award-number":["IST-2005-016004"]}],"id":[{"id":"10.13039\/501100004965","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2012,6]]},"abstract":"<jats:p>We introduce a logical verification methodology for checking behavioral properties of service-oriented computing systems. Service properties are described by means of SocL, a branching-time temporal logic that we have specifically designed for expressing in an effective way distinctive aspects of services, such as, acceptance of a request, provision of a response, correlation among service requests and responses, etc. Our approach allows service properties to be expressed in such a way that they can be independent of service domains and specifications. We show an instantiation of our general methodology that uses the formal language COWS to conveniently specify services and the expressly developed software tool CMC to assist the user in the task of verifying SocL formulas over service specifications. We demonstrate the feasibility and effectiveness of our methodology by means of the specification and analysis of a case study in the automotive domain.<\/jats:p>","DOI":"10.1145\/2211616.2211619","type":"journal-article","created":{"date-parts":[[2012,7,3]],"date-time":"2012-07-03T11:53:04Z","timestamp":1341316384000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["A logical verification methodology for service-oriented computing"],"prefix":"10.1145","volume":"21","author":[{"given":"Alessandro","family":"Fantechi","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Firenze, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[{"name":"Istituto di Scienza e Tecnologie dell'Informazione \u201cA. Faedo\u201d, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Lapadula","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Firenze, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[{"name":"Istituto di Scienza e Tecnologie dell'Informazione \u201cA. Faedo\u201d, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rosario","family":"Pugliese","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Firenze, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Tiezzi","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Firenze, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,7,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1420446.1420478"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Alonso G. Casati F. Kuno H. A. and Machiraju V. 2004. Web Services\u2014Concepts Architectures and Applications. Data-Centric systems and applications. Springer. Alonso G. Casati F. Kuno H. A. and Machiraju V. 2004. Web Services\u2014Concepts Architectures and Applications. Data-Centric systems and applications. Springer.","DOI":"10.1007\/978-3-662-10876-5"},{"key":"e_1_2_1_3_1","volume-title":"International Conference on Dependable Systems and Networks. IEEE Computer Society","author":"Baier C."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.08.005"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Bhat G. Cleaveland R. and Grumberg O. 1995. Efficient on-the-fly model checking for CTL*. In LICS. IEEE Computer Society Los Alamitos CA 388--397. Bhat G. Cleaveland R. and Grumberg O. 1995. Efficient on-the-fly model checking for CTL*. In LICS. IEEE Computer Society Los Alamitos CA 388--397.","DOI":"10.1109\/LICS.1995.523273"},{"key":"e_1_2_1_6_1","unstructured":"Bocchi L. Fantechi A. G\u00f6nczy L. and Koch N. 2006. Prototype language for service modelling: SOA ontology in structured natural language. Sensoria deliverable D1.1a. Bocchi L. Fantechi A. G\u00f6nczy L. and Koch N. 2006. Prototype language for service modelling: SOA ontology in structured natural language. Sensoria deliverable D1.1a."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.09.025"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68863-1_3"},{"key":"e_1_2_1_9_1","first-page":"207","article-title":"JACK: Just another concurrency kit. The integration","volume":"54","author":"Bouali A.","year":"1994","journal-title":"Project. Bull. EATCS"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Bradfield J. and Stirling C. 2001. Modal logics and mu-calculi: An introduction Handbook of Process Algebra Bergstra J. A. Ponse A. and Smolka A. Eds. North-Holland Chapter 293--330. Bradfield J. and Stirling C. 2001. Modal logics and mu-calculi: An introduction Handbook of Process Algebra Bergstra J. A. Ponse A. and Smolka A. Eds. North-Holland Chapter 293--330.","DOI":"10.1016\/B978-044482830-9\/50022-9"},{"key":"e_1_2_1_11_1","volume-title":"Eds. LNCS Series","volume":"5052","author":"Bruni R."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11767954_5"},{"key":"e_1_2_1_13_1","volume-title":"ESOP. LNCS Series","volume":"4421","author":"Carbone M."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11589976_5"},{"key":"e_1_2_1_15_1","volume-title":"IFM. LNCS Series","volume":"2999","author":"Chaki S."},{"key":"e_1_2_1_16_1","volume-title":"Logic of Programs. LNCS Series","volume":"131","author":"Clarke E."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_18_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. The MIT Press Cambridge MA. Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. The MIT Press Cambridge MA."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0072"},{"key":"e_1_2_1_20_1","volume-title":"Logic for Concurrency and Synchronisation. Trends in Logic","author":"Dam M."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.05.008"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/963927.963930"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.05.019"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the Ecole de Printemps on Semantics of Concurrency. LNCS Series","volume":"469","author":"De Nicola R."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"key":"e_1_2_1_27_1","volume-title":"FASE. LNCS Series","volume":"4961","author":"Fantechi A."},{"key":"e_1_2_1_28_1","unstructured":"Fantechi A. Gnesi S. Lapadula A. Mazzanti F. Pugliese R. and Tiezzi F. 2010. Specification and analysis of an automotive scenario. Tech. rep. DSI Universit\u00e0 di Firenze. http:\/\/rap.dsi.unifi.it\/cows\/papers\/automotiveScenario_in_cows.pdf. Fantechi A. Gnesi S. Lapadula A. Mazzanti F. Pugliese R. and Tiezzi F. 2010. Specification and analysis of an automotive scenario. Tech. rep. DSI Universit\u00e0 di Firenze. http:\/\/rap.dsi.unifi.it\/cows\/papers\/automotiveScenario_in_cows.pdf."},{"key":"e_1_2_1_29_1","volume-title":"CAV. LNCS Series","volume":"1102","author":"Fernandez J."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/990010.990013"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2163252.2163267"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2005.141"},{"key":"e_1_2_1_33_1","volume-title":"Perspectives. LNCS Series","volume":"5000","author":"Grumberg O."},{"key":"e_1_2_1_34_1","unstructured":"Gudgin M. Hadley M. and Rogers T. 2006. Web Services Addressing 1.0 - Core. Tech. rep. W3C. May. W3C Recommendation. Gudgin M. Hadley M. and Rogers T. 2006. Web Services Addressing 1.0 - Core. Tech. rep. W3C. May. W3C Recommendation."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11948148_27"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050020"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_38_1","unstructured":"Kavantzas N. Burdett D. and Ritzinger G. 2004. Web services choreography description language version 1.0. Tech. rep. W3C. http:\/\/www.w3.org\/TR\/ws-cdl-10\/. Kavantzas N. Burdett D. and Ritzinger G. 2004. Web services choreography description language version 1.0. Tech. rep. W3C. http:\/\/www.w3.org\/TR\/ws-cdl-10\/."},{"key":"e_1_2_1_39_1","series-title":"LNCS Series","volume-title":"ESTL: A temporal logic for events and states. In Application and Theory of Petri Nets","author":"Kindler E.","year":"1998"},{"key":"e_1_2_1_40_1","unstructured":"Koch N. 2007. Automotive case study: UML specification of on road assistance scenario. Sensoria report http:\/\/rap.dsi.unifi.it\/sensoria\/files\/FAST_report_1_2007_ACS_UML.pdf. Koch N. 2007. Automotive case study: UML specification of on road assistance scenario. Sensoria report http:\/\/rap.dsi.unifi.it\/sensoria\/files\/FAST_report_1_2007_ACS_UML.pdf."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.13"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11767954_10"},{"key":"e_1_2_1_43_1","volume-title":"ESOP. LNCS Series","volume":"4421","author":"Lapadula A."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68679-8_43"},{"key":"e_1_2_1_45_1","volume-title":"FORTE. IFIP Conference Proceedings Series","volume":"69","author":"Lawford M."},{"key":"e_1_2_1_46_1","volume-title":"Symposium on Protocol Specification, Testing and Verification. North-Holland, 79--92","author":"Lin H.","year":"1993"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_12"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/EDOC.2008.55"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2007.10.023"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/944217.944236"},{"key":"e_1_2_1_51_1","unstructured":"Moller F. and Stevens P. 1999. Edinburgh Concurrency Workbench User Manual. http:\/\/homepages.inf.ed.ac.uk\/perdita\/cwb\/. Moller F. and Stevens P. 1999. Edinburgh Concurrency Workbench User Manual. http:\/\/homepages.inf.ed.ac.uk\/perdita\/cwb\/."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/647168.718138"},{"key":"e_1_2_1_53_1","unstructured":"OASIS WSBPEL TC. 2007. Web services business process execution language version 2.0. Tech. rep. OASIS. April. http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/OS\/wsbpel-v2.0-OS.html. OASIS WSBPEL TC. 2007. Web services business process execution language version 2.0. Tech. rep. OASIS. April. http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/OS\/wsbpel-v2.0-OS.html."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74128-2_8"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.06.008"},{"key":"e_1_2_1_56_1","unstructured":"SENSORIA. 2005. Software engineering for service-oriented overlay computers. http:\/\/sensoria.fast.de. SENSORIA. 2005. Software engineering for service-oriented overlay computers. http:\/\/sensoria.fast.de."},{"key":"e_1_2_1_57_1","doi-asserted-by":"crossref","unstructured":"Stirling C. 2001. Modal and Temporal Properties of Processes. Springer. Stirling C. 2001. Modal and Temporal Properties of Processes. Springer.","DOI":"10.1007\/978-1-4757-3550-5"},{"key":"e_1_2_1_58_1","volume-title":"TAPSOFT. LNCS Series","volume":"354","author":"Stirling C."},{"key":"e_1_2_1_59_1","volume-title":"FMICS. LNCS Series","volume":"4916","author":"Beek M."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368173"},{"key":"e_1_2_1_61_1","unstructured":"Tiezzi F. 2009. Specification and analysis of service-oriented applications. Ph.D. thesis Dipartimento di Sistemi e Informatica Universit\u00e0 degli Studi di Firenze. http:\/\/rap.dsi.unifi.it\/cows. Tiezzi F. 2009. Specification and analysis of service-oriented applications. Ph.D. thesis Dipartimento di Sistemi e Informatica Universit\u00e0 degli Studi di Firenze. http:\/\/rap.dsi.unifi.it\/cows."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_7"},{"key":"e_1_2_1_63_1","unstructured":"van Breugel F. and Koshkina M. 2006. Models and verification of BPEL. Tech. rep. Department of Computer Science and Engineering York University. http:\/\/www.cse.yorku.ca\/~franck\/research\/drafts\/tutorial.pdf. van Breugel F. and Koshkina M. 2006. Models and verification of BPEL. Tech. rep. Department of Computer Science and Engineering York University. http:\/\/www.cse.yorku.ca\/~franck\/research\/drafts\/tutorial.pdf."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022883727209"},{"key":"e_1_2_1_65_1","volume-title":"CAV. LNCS Series","volume":"818","author":"Victor B."},{"key":"e_1_2_1_66_1","volume-title":"ESOP. LNCS Series","volume":"4960","author":"Vieira H."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0136-3"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2211616.2211619","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2211616.2211619","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:21:05Z","timestamp":1750238465000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2211616.2211619"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":67,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["10.1145\/2211616.2211619"],"URL":"https:\/\/doi.org\/10.1145\/2211616.2211619","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6]]},"assertion":[{"value":"2008-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-07-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}