{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:32:25Z","timestamp":1750307545763,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,10,17]],"date-time":"2009-10-17T00:00:00Z","timestamp":1255737600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["60673116"],"award-info":[{"award-number":["60673116"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002855","name":"Ministry of Science and Technology of the People's Republic of China","doi-asserted-by":"publisher","award":["2006AA01Z166","2009CB320700"],"award-info":[{"award-number":["2006AA01Z166","2009CB320700"]}],"id":[{"id":"10.13039\/501100002855","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2009,10,17]]},"DOI":"10.1145\/1640206.1640225","type":"proceedings-article","created":{"date-parts":[[2009,10,27]],"date-time":"2009-10-27T13:27:28Z","timestamp":1256650048000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal verification of service composition in pervasive computing environments"],"prefix":"10.1145","author":[{"given":"Junqing","family":"Chen","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Linpeng","family":"Huang","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,10,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1038\/scientificamerican0991-94"},{"volume-title":"Proceedings of the 7th personal wireless communications conference","author":"Chakraborty D.","key":"e_1_3_2_1_2_1","unstructured":"Chakraborty , D. , Perich , F. , Joshi , A. , Finin , T. , and Yesha , Y . 2002. A reactive service composition architecture for pervasive computing environments . In: Proceedings of the 7th personal wireless communications conference , Singapore, 53--62. Chakraborty, D., Perich, F., Joshi, A., Finin, T., and Yesha, Y. 2002. A reactive service composition architecture for pervasive computing environments. In: Proceedings of the 7th personal wireless communications conference, Singapore, 53--62."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90339-H"},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of Asia-Pacific Software Engineering Conference APSEC","author":"Okazaki M.","year":"2002","unstructured":"Okazaki , M. , Aoki , T. , and Katayama , T . 2002. Extracting threads from concurrent objects for the design of embedded systems , In Proceedings of Asia-Pacific Software Engineering Conference APSEC 2002 , 107--116. Okazaki, M., Aoki, T., and Katayama, T. 2002. Extracting threads from concurrent objects for the design of embedded systems, In Proceedings of Asia-Pacific Software Engineering Conference APSEC 2002, 107--116."},{"volume-title":"Proc. 27th Australasian Computer Science Conference (ACSC2004)","author":"Jansamak S.","key":"e_1_3_2_1_5_1","unstructured":"Jansamak , S. , and Surarerks , A . 2004. Formalization of UML Statechart Models Using Concurrent Regular Expressions . In Proc. 27th Australasian Computer Science Conference (ACSC2004) , Dunedin, New Zealand, CRPIT, 26. Estivill-Castro, V., Ed. ACS, 83--88. Jansamak, S., and Surarerks, A. 2004. Formalization of UML Statechart Models Using Concurrent Regular Expressions. In Proc. 27th Australasian Computer Science Conference (ACSC2004), Dunedin, New Zealand, CRPIT, 26. Estivill-Castro, V., Ed. ACS, 83--88."},{"key":"e_1_3_2_1_6_1","volume-title":"2nd Int. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols","author":"Vijay K. G.","year":"1989","unstructured":"Vijay , K. G. 1989 . Modeling of distribute systems by concurrent regular expressions . In 2nd Int. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols , Vancouver, Canada. Vijay, K. G. 1989. Modeling of distribute systems by concurrent regular expressions. In 2nd Int. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols, Vancouver, Canada."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Campbell R. H. and \n      Habermann A. N\n  . \n  1974\n  . The specification of process synchronization by path expressions. In E. Gelenbe and C. Kaiser editors Int. Symp. on Operating Systems volume \n  16\n   of \n  LNCS . \n  Springer-Verlag 89--102.   Campbell R. H. and Habermann A. N. 1974. The specification of process synchronization by path expressions. In E. Gelenbe and C. Kaiser editors Int. Symp. on Operating Systems volume 16 of LNCS . Springer-Verlag 89--102.","DOI":"10.1007\/BFb0029355"},{"key":"e_1_3_2_1_8_1","unstructured":"Jeff M. and Jeff K. 2006. Concurrency: state models and java programs. John Wiley New York NY USA Second Edition.   Jeff M. and Jeff K. 2006. Concurrency: state models and java programs. John Wiley New York NY USA Second Edition."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287657"},{"key":"e_1_3_2_1_10_1","unstructured":"Breugel F. V. and Koshkina M. 2006. Models and Verification of BPEL Technical Report York University Toronto Canada (2006) http:\/\/www.cse.yorku.ca\/~franck\/research\/drafts\/tutorial.pdf.  Breugel F. V. and Koshkina M. 2006. Models and Verification of BPEL Technical Report York University Toronto Canada (2006) http:\/\/www.cse.yorku.ca\/~franck\/research\/drafts\/tutorial.pdf."},{"key":"e_1_3_2_1_11_1","volume-title":"Model-based Verification of Web Service Compositions","author":"Foster H.","year":"2003","unstructured":"Foster , H. , Uchitel , S., J Kramer , J. , Magee , J. 2003. Model-based Verification of Web Service Compositions . IEEE Automated Software Engineering (ASE) 2003 , Montreal, Canada . Foster, H., Uchitel, S., J Kramer, J., Magee, J. 2003. Model-based Verification of Web Service Compositions. IEEE Automated Software Engineering (ASE) 2003, Montreal, Canada."},{"key":"e_1_3_2_1_12_1","volume-title":"Pervasive Services Engineering for SOAs. ICSOC PhD Symposium 2008, 6th International Conference on Service Oriented Computing, December 1--5","author":"Dhaminda A.","year":"2008","unstructured":"Dhaminda A. 2008 . Pervasive Services Engineering for SOAs. ICSOC PhD Symposium 2008, 6th International Conference on Service Oriented Computing, December 1--5 , 2008, University of Technology, Sydney. Dhaminda A. 2008. Pervasive Services Engineering for SOAs. ICSOC PhD Symposium 2008, 6th International Conference on Service Oriented Computing, December 1--5, 2008, University of Technology, Sydney."},{"volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann G. J.","key":"e_1_3_2_1_14_1","unstructured":"Holzmann , G. J. 2004. The Spin Model Checker: Primer and Reference Manual . Addison-Wesley , Boston, MA, USA . Holzmann, G. J. 2004. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Boston, MA, USA."},{"key":"e_1_3_2_1_15_1","unstructured":"Jeff M. Jeff K. Robert C. Sebastian U. and Howard F. 2009. Labelled Transition System Analyser (LTSA v3.0). http:\/\/www.doc.ic.ac.uk\/ltsa\/.  Jeff M. Jeff K. Robert C. Sebastian U. and Howard F. 2009. Labelled Transition System Analyser (LTSA v3.0). http:\/\/www.doc.ic.ac.uk\/ltsa\/."},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","volume-title":"WSAT: A tool for formal analysis of web services","author":"Xiang F.","year":"2004","unstructured":"Xiang , F. , Tevfik , B. , and Jianwen , S . 2004 . WSAT: A tool for formal analysis of web services . In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, volume 3114 of LNCS , Springer-Verlag , 510--514. Xiang, F., Tevfik, B., and Jianwen, S. 2004. WSAT: A tool for formal analysis of web services. In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, volume 3114 of LNCS, Springer-Verlag, 510--514."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_2"}],"event":{"name":"Internetware '09: First Asia-Pacific Symposium on Internetware","sponsor":["CCF China Computer Federation","SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Beijing China","acronym":"Internetware '09"},"container-title":["Proceedings of the First Asia-Pacific Symposium on Internetware"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1640206.1640225","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1640206.1640225","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:23:30Z","timestamp":1750249410000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1640206.1640225"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10,17]]},"references-count":16,"alternative-id":["10.1145\/1640206.1640225","10.1145\/1640206"],"URL":"https:\/\/doi.org\/10.1145\/1640206.1640225","relation":{},"subject":[],"published":{"date-parts":[[2009,10,17]]},"assertion":[{"value":"2009-10-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}