{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T15:26:56Z","timestamp":1767626816504,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001980"},{"type":"electronic","value":"9783540361893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36189-8_15","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T13:46:00Z","timestamp":1188308760000},"page":"188-202","source":"Crossref","is-referenced-by-count":31,"title":["Formal Verification of e-Services and Workflows"],"prefix":"10.1007","author":[{"given":"Xiang","family":"Fu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianwen","family":"Su","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"issue":"3","key":"15_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"R. Alur, T. A. Henzinger, and P. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3): 181\u2013201, March 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"T. Bultan. Action language: A specification language for model checking reactive systems. In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), pages 335\u2013344, June 2000.","DOI":"10.1145\/337180.337219"},{"issue":"4","key":"15_CR3","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747\u2013789, July 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. In IEEE Symposium on Logic in Computer Science, pages 428\u2013439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"issue":"3","key":"15_CR5","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/S0306-4379(01)00014-X","volume":"26","author":"F. Casati","year":"2001","unstructured":"F. Casati and M.-C. Shan. Dynamic and adaptive composition of e-services. Information Systems, 26(3):143\u2013163, 2001.","journal-title":"Information Systems"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"V. Christophides, R. Hull, G. Karvounarakis, A. Kumar, G. Tong, and M. Xiong. Beyond discrete e-services: Composing session-oriented services in telecommunications. In Proc. of Workshop on Technologies for E-Services (TES), Rome, Italy, Sept. 2001.","DOI":"10.1007\/3-540-44809-8_5"},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Logic of Programs: Workshop","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In D. Kozen, editor, Logic of Programs: Workshop, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, May 1981."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"H. Davulcu, M. Kifer, C.R. Ramakrishnan, and I.V. Ramakrishnan. Logic based modeling and analysis. Inpods, 1998.","DOI":"10.1145\/275487.275491"},{"key":"15_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"G. Delzanno. Automatic verification of parameterized cache coherence protocols. In Proceedings of the 12th International Conference on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 53\u201368. Springer-Verlag, 2000."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"G. Delzanno and T. Bultan. Constraint-based verification of client-server protocols. In Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming, 2001.","DOI":"10.1007\/3-540-45578-7_20"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"M. C. Fauvet, M. Dumas, B. Benatallah, and H. Y. Paik. Peer-to-peer traced execution of composite services. In Proc. ofWorkshop on Technologies for E-Services (TES), Rome, Italy, Sept. 2001.","DOI":"10.1007\/3-540-44809-8_8"},{"key":"15_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-45319-9_11","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"X. Fu","year":"2001","unstructured":"X. Fu, T. Bultan, R. Hull, and J. Su. Verification of vortex workflows. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 143\u2013157. Springer-Verlag, April 2001."},{"key":"15_CR13","unstructured":"X. Fu, T. Bultan, and J. Su. Hybrid predicate abstraction for verification of workflow and decision flow systems. Technical report, Computer Science Department, UCSB, January 2002."},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/3-540-46439-5_12","volume-title":"Proceedings of the 7th International Conference on Extending Database Technology","author":"M. Gillmann","year":"2000","unstructured":"M. Gillmann, J. Weissenfels, G. Weikum, and A. Kraiss. Performance and availability assessment for the configuration of distributed workflow management systems. In Proceedings of the 7th International Conference on Extending Database Technology, LNCS 1777, pages 183\u2013202, 2000."},{"key":"15_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-56922-7_36","volume-title":"Proceedings of the 2nd Workshop on Computer Aided Verification","author":"P. Godefroid","year":"1993","unstructured":"P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In Proceedings of the 2nd Workshop on Computer Aided Verification, LNCS 697, pages 438\u2013449, 1993."},{"key":"15_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of International Symposium on Static Analysis","author":"N. Halbwachs","year":"1994","unstructured":"N. Halbwachs, P. Raymond, and Y. Proy. Verification of linear hybrid systems by means of convex approximations. In B. LeCharlier, editor, Proceedings of International Symposium on Static Analysis, volume 864 of Lecture Notes in Computer Science, Springer-Verlag, September 1994."},{"issue":"5","key":"15_CR17","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"R. Hull, F. Llirbat, E. Simon, J. Su, G. Dong, B. Kumar, and G. Zhou. Declarative workflows that support easy modification and dynamic browsing. In Proc. Int. Joint Conf. on Work Activities Coordination and Collaboration, 1999.","DOI":"10.1145\/295665.295674"},{"key":"15_CR19","volume-title":"Technical Report","author":"W. Kelly","year":"1995","unstructured":"W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The Omega library interface guide. Technical Report CS-TR-3445, Department of Computer Science, University of Maryland, College Park, March 1995."},{"issue":"1","key":"15_CR20","first-page":"58","volume":"24","author":"A. Kraiss","year":"2001","unstructured":"A. Kraiss, F. Sch\u00f6n, G. Weikum, and U. Deppisch. Towards response time guarantees for e-service middleware. IEEE Data Engineering Bulletin, 24(1):58\u201363, 2001.","journal-title":"IEEE Data Engineering Bulletin"},{"key":"15_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K. L. McMillan","year":"1993","unstructured":"K. L. McMillan. Symbolic model checking. Kluwer Academic Publishers, Massachusetts, 1993."},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"P. Muth, D. Wodtke, J. Weissenfels, G. Weikum, and A. Kotz-Dittrich. Enterprise-wide workflow management based on state and activity charts. In Proc. NATO Advanced Study Institute on Workflow Management Systems and Interoperability, 1997.","DOI":"10.1145\/253260.253411"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"D. C. Oppen","year":"1978","unstructured":"D. C. Oppen. A 22 2 2 pn upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences, 16:323\u2013332, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"15_CR24","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. In Proceedings of the 18th Symposium on Foundations of Computer Science, 1977."},{"key":"15_CR25","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Graph-based algorithms for boolean function manipulation. In Proceedings of the 27th ACM\/IEEE Design Automation Conference, 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"15_CR27","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Statica Analysis Symposium","author":"H. Saidi","year":"2000","unstructured":"H. Saidi. Model checking guided abstraction and analysis. In Proceedings of Statica Analysis Symposium, Lecture Notes in Computer Science. Springer, 2000."},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"M. Schroeder. Verification of business processes for a correspondence handling center using CCS. In Proc. European Symp. on Validation and Verification of Knowledge Based Systems and Components, June 1999.","DOI":"10.1007\/978-1-4757-6916-6_17"},{"issue":"1","key":"15_CR29","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"W. M. P. Aalst van der","year":"1998","unstructured":"W. M. P. van der Aalst. The application of petri nets to workflow management. Journal of Circuits, systems and computers, 8(1):21\u201326, 1998.","journal-title":"Journal of Circuits, systems and computers"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"W. M. P. van der Aalst and A. H. M. ter Hofstede. Verification of workflow task structures: A Petri-net-based approach. Information Systems, 25(1), 2000.","DOI":"10.1016\/S0306-4379(00)00008-9"},{"key":"15_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-45319-9_5","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Yavuz-Kahveci","year":"2001","unstructured":"T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. Composite symbolic library. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 335\u2013344. Springer-Verlag, April 2001."}],"container-title":["Lecture Notes in Computer Science","Web Services, E-Business, and the Semantic Web"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36189-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T18:06:50Z","timestamp":1737396410000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36189-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001980","9783540361893"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-36189-8_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}