{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:40:30Z","timestamp":1775054430964,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,5,10]],"date-time":"2008-05-10T00:00:00Z","timestamp":1210377600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2008,5,10]]},"DOI":"10.1145\/1368088.1368173","type":"proceedings-article","created":{"date-parts":[[2008,5,15]],"date-time":"2008-05-15T14:36:48Z","timestamp":1210862208000},"page":"613-622","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Formal verification of an automotive scenario in service-oriented computing"],"prefix":"10.1145","author":[{"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[{"name":"CNR, Pisa, Italy"}]},{"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[{"name":"CNR, Pisa, Italy"}]},{"given":"Nora","family":"Koch","sequence":"additional","affiliation":[{"name":"Cirquent GmbH, Munich, Germany"}]},{"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[{"name":"CNR, Pisa, Italy"}]}],"member":"320","published-online":{"date-parts":[[2008,5,10]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009382.1009786"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECOWS.2006.22"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","unstructured":"M.H. ter Beek A. Fantechi S. Gnesi and F. Mazzanti. An action\/state-based model-checking approach for the analysis of communication protocols for Service-Oriented Applications. To appear in Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'07) Berlin Germany volume 4916 of Lecture Notes in Computer Science. Springer Berlin 2008.","DOI":"10.5555\/1793603.1793616"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/788017.788743"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0071-z"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.05.008"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/111693.111710"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792838.1792860"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647765.735847"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2008.7.1.a1"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 2nd International Conference on Software Engineering Research, Management & Applications (SERA'04)","author":"Gnesi S.","year":"2004","unstructured":"S. Gnesi and F. Mazzanti. On the y model checking of communicating UML State Machines. In Proceedings of the 2nd International Conference on Software Engineering Research, Management & Applications (SERA'04), Los Angeles, CA, USA, pages 331--338, 2004."},{"key":"e_1_3_2_1_14_1","volume-title":"XLIII Annual Italian Conference AICA","author":"Gnesi S.","year":"2005","unstructured":"S. Gnesi and F. Mazzanti. A Model Checking Verification Environment for UML Statecharts. Presented at the XLIII Annual Italian Conference AICA, Udine, 2005."},{"key":"e_1_3_2_1_15_1","volume-title":"September","author":"G\u00f6nczy L.","year":"2007","unstructured":"L. G\u00f6nczy and D. Varr\u00f3. Model-Driven Transformations for Deployment|Prototype. Sensoria Deliverable 6.4a, September 2007. Available via {31}."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/647982.743551"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645395.651926"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647745.734059"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/646847.707098"},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Informatics","first-page":"115","volume-title":"Proceedings of Modellierung 2006 (MOD'06), Innsbruck, Austria","author":"Knapp A.","year":"2006","unstructured":"A. Knapp and G. Zhang. Model Transformations for Integrating and Validating Web Application Models. In H.C. Mayr and R. Breu, editors, Proceedings of Modellierung 2006 (MOD'06), Innsbruck, Austria, volume 82 of Lecture Notes in Informatics, pages 115--128. Gesellschaft f\u00fcr Informatik, Bonn, 2006."},{"key":"e_1_3_2_1_22_1","volume-title":"September","author":"Koch N.","year":"2007","unstructured":"N. Koch and D. Berndl. Requirements Modelling and Analysis of Selected Scenarios of the Automative Case Study. Sensoria Deliverable 8.2a, September 2007. Available via {31}."},{"key":"e_1_3_2_1_23_1","volume-title":"September","author":"Koch N.","year":"2007","unstructured":"N. Koch, P. Mayer, R. Heckel, L. G\u00fcnczy and C. Montangero. UML for Service-Oriented Systems. Sensoria Deliverable 1.4a, September 2007. Available via {31}."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002870050102"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_3_2_1_26_1","unstructured":"F. Mazzanti. UMC User Guide v3.3. Technical Report 2006-TR-33 Istituto di Scienza e Tecnologie dell'Informazione \\A. Faedo\" CNR 2006. http:\/\/fmt.isti.cnr.it\/WEBPAPER\/UMC-UG33.pdf"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2007.10.023"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/647168.718138"},{"key":"e_1_3_2_1_29_1","volume-title":"JavaSPEKTRUM. SIGS Datacom","author":"Saad A.","year":"2003","unstructured":"A. Saad. Java-based Functionality and Data Management in the automobile|Prototyping at BMW Car IT GmbH. JavaSPEKTRUM. SIGS Datacom, March 2003."},{"key":"e_1_3_2_1_30_1","unstructured":"SCADE suite. http:\/\/www.estereltechnologies. com\/products\/scade-suite\/"},{"key":"e_1_3_2_1_31_1","unstructured":"EU project Sensoria (IST-2005-016004). http:\/\/www.sensoria-ist.eu\/"},{"key":"e_1_3_2_1_32_1","unstructured":"SPARK toolset. http:\/\/www.praxis-his.com\/sparkada\/"},{"key":"e_1_3_2_1_33_1","unstructured":"Spin model checker. http:\/\/www.spinroot.com"},{"key":"e_1_3_2_1_34_1","unstructured":"UMC model checker. http:\/\/fmt.isti.cnr.it\/umc\/"},{"key":"e_1_3_2_1_35_1","unstructured":"Unified Modeling Language. http:\/\/www.uml.org\/"},{"key":"e_1_3_2_1_36_1","unstructured":"Uppaal tool. http:\/\/www.uppaal.com"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11888116_3"}],"event":{"name":"ICSE '08: International Conference on Software Engineering","location":"Leipzig Germany","acronym":"ICSE '08","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 30th international conference on Software engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1368088.1368173","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1368088.1368173","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T13:49:40Z","timestamp":1773582580000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1368088.1368173"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5,10]]},"references-count":37,"alternative-id":["10.1145\/1368088.1368173","10.1145\/1368088"],"URL":"https:\/\/doi.org\/10.1145\/1368088.1368173","relation":{},"subject":[],"published":{"date-parts":[[2008,5,10]]},"assertion":[{"value":"2008-05-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}