{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:43:31Z","timestamp":1725515011924},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540686439"},{"type":"electronic","value":"9783540686446"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-68644-6_13","type":"book-chapter","created":{"date-parts":[[2008,6,9]],"date-time":"2008-06-09T04:59:41Z","timestamp":1212987581000},"page":"179-193","source":"Crossref","is-referenced-by-count":14,"title":["Formal Modeling and Discrete-Time Analysis of BPEL Web Services"],"prefix":"10.1007","author":[{"given":"Radu","family":"Mateescu","sequence":"first","affiliation":[]},{"given":"Sylvain","family":"Rampacek","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"13_CR2","first-page":"457","volume-title":"Proc. of WI 2005","author":"A. Chirichiello","year":"2005","unstructured":"Chirichiello, A., Sala\u00fcn, G.: Encoding abstract descriptions into executable web services: Towards a formal development. In: Proc. of WI 2005, pp. 457\u2013463. IEEE Computer Society, Los Alamitos (2005)"},{"key":"13_CR3","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Ferrara, A.: Web services: a process algebra approach. In: ICSOC, pp. 242\u2013251 (2004)","DOI":"10.1145\/1035167.1035202"},{"key":"13_CR5","volume-title":"Proc. of the 13th International World Wide Web Conference (WWW 2004)","author":"X. Fu","year":"2004","unstructured":"Fu, X., Bultan, T., Su, J.: Analysis of interacting BPEL web services. In: Proc. of the 13th International World Wide Web Conference (WWW 2004), USA, ACM Press, New York (2004)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_48","volume-title":"Computer Aided Verification","author":"X. Fu","year":"2004","unstructured":"Fu, X., Bultan, T., Su, J.: WSAT: A tool for formal analysis of web services. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/C\u00c6SAR: An open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, pp. 68\u201384. Springer, Heidelberg (1998)"},{"key":"13_CR8","first-page":"377","volume-title":"Proc. of FORTE 2001","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Proc. of FORTE 2001, IFIP, pp. 377\u2013392. Kluwer Academic Publishers, Dordrecht (2001); Full version available as INRIA Research Report\u00a0RR-4223"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-540-73368-3_18","volume-title":"Computer Aided Verification","author":"H. Garavel","year":"2007","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 158\u2013163. Springer, Heidelberg (2007)"},{"key":"13_CR10","unstructured":"Object\u00a0Management Group. Business process modeling notation (BPMN) specification (May 2006)"},{"key":"13_CR11","unstructured":"Haddad, S., Melliti, T., Moreaux, P., Rampacek, S.: Modelling web services interoperability. In: Proc. of the 6th Int. Conf. on Enterprise Information Systems (ICEIS 2004), Porto, Portugal (April14\u201317, 2004)"},{"key":"13_CR12","series-title":"Lecture Notes in Business Information Processing","volume-title":"ICEIS 2006, Revised Selected Paper","author":"S. Haddad","year":"2008","unstructured":"Haddad, S., Moreaux, P., Rampacek, S.: A formal semantics and a client synthesis for a BPEL service. In: ICEIS 2006, Revised Selected Paper. Lecture Notes in Business Information Processing, vol.\u00a03, Springer, Heidelberg (2008)"},{"key":"13_CR13","unstructured":"ISO\/IEC. LOTOS \u2014 a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807, International Organization for Standardization \u2014 Information Processing Systems \u2014 Open Systems Interconnection, Gen\u00e8ve (September 1989)"},{"key":"13_CR14","unstructured":"Jordan, D., Evdemon, J.: Web Services Business Process Execution Language Version 2.0 - Oasis Standard (April 11, 2007)"},{"key":"13_CR15","unstructured":"Josuttis, N.: Soa in Practice \u2013 The Art of Distributed System Design, O\u2019Reilly Media, City (2007)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11589976_6","volume-title":"Integrated Formal Methods","author":"F. Lang","year":"2005","unstructured":"Lang, F.: EXP.OPEN 2.0: A flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol.\u00a03771, Springer, Heidelberg (2005)"},{"issue":"1\u20132","key":"13_CR17","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer\u00a01(1\u20132), 134\u2013152 (1997)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"13_CR18","volume-title":"Concurrency: State Models and Java Programs","author":"J. Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. Wiley, Chichester (1999)"},{"issue":"4","key":"13_CR19","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/BF01660034","volume":"1","author":"A.J. Martin","year":"1986","unstructured":"Martin, A.J.: Compiling communicating processes into delay-insensitive VLSI circuits. Distributed Computing\u00a01(4), 226\u2013234 (1986)","journal-title":"Distributed Computing"},{"issue":"3","key":"13_CR20","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Science of Computer Programming\u00a046(3), 255\u2013281 (2003)","journal-title":"Science of Computer Programming"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of FM 2008","author":"R. Mateescu","year":"2008","unstructured":"Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Proc. of FM 2008. LNCS, vol.\u00a05014, Springer, Heidelberg (2008)"},{"key":"13_CR22","volume-title":"Proc. of ECOWS 2006","author":"T. Melliti","year":"2006","unstructured":"Melliti, T., Boutrous-Saab, C., Rampacek, S.: Verifying correctness of web services choreography. In: Proc. of ECOWS 2006, Zurich, Switzerland, IEEE Computer Society Press, Los Alamitos (2006)"},{"issue":"1-2","key":"13_CR23","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0167-6423(96)00033-0","volume":"29","author":"M.J. Morley","year":"1997","unstructured":"Morley, M.J.: Safety-level communication in railway interlockings. Science of Computer Programming\u00a029(1-2), 147\u2013170 (1997)","journal-title":"Science of Computer Programming"},{"issue":"1","key":"13_CR24","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1006\/inco.1994.1083","volume":"114","author":"X. Nicollin","year":"1994","unstructured":"Nicollin, X., Sifakis, J.: The algebra of timed processes ATP: Theory and application (1994)","journal-title":"Information and Computation"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-540-30209-4_15","volume-title":"Web Services","author":"G. Sala\u00fcn","year":"2004","unstructured":"Sala\u00fcn, G., Ferrara, A., Chirichiello, A.: Negotiation Among Web Services Using LOTOS\/CADP. In: (LJ) Zhang, L.-J., Jeckle, M. (eds.) ECOWS 2004. LNCS, vol.\u00a03250, pp. 198\u2013212. Springer, Heidelberg (2004)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1007\/978-3-540-73210-5_29","volume-title":"Integrated Formal Methods","author":"G. Sala\u00fcn","year":"2007","unstructured":"Sala\u00fcn, G., Kramer, J., Lang, F., Magee, J.: Translating FSP into LOTOS and networks of automata. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 558\u2013578. Springer, Heidelberg (2007)"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/11589976_17","volume-title":"Proc. of IFM 2005","author":"G. Sala\u00fcn","year":"2005","unstructured":"Sala\u00fcn, G., Serwe, W.: Translating hardware process algebras into standard process algebras \u2014 illustration with CHP and LOTOS. In: Proc. of IFM 2005. LNCS, vol.\u00a03371, pp. 287\u2013306. Springer, Heidelberg (2005)"},{"issue":"2","key":"13_CR28","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1016\/j.jnca.2006.02.001","volume":"30","author":"K.J. Turner","year":"2007","unstructured":"Turner, K.J.: Representing and analysing composed web services using CRESS. J. Netw. Comput. Appl.\u00a030(2), 541\u2013562 (2007)","journal-title":"J. Netw. Comput. Appl."}],"container-title":["Lecture Notes in Business Information Processing","Advances in Enterprise Engineering I"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68644-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T01:27:54Z","timestamp":1557624474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68644-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540686439","9783540686446"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68644-6_13","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2008]]}}}