Verification of Web Service Compositions: An Operationalization of Correctness and a Requirements Framework for Service-oriented Modeling Techniques
Tóm tắt
Web service compositions coordinate Web services of different enterprises. They are expected to constitute the foundation of service-oriented architectures, to improve business processes as well as to foster intra- and inter-organizational integration. Especially in inter-organizational contexts, quality of service referring to non-functional requirements and conformance to functional requirements are becoming vital properties. With Web service compositions being asynchronous and distributed systems, the latter property – which is also called correctness – can be shown best by verification. This paper examines from a system-theoretic perspective how correctness can be operationalized for Web service compositions. It also proposes a requirements framework for service-oriented modeling techniques so that correctness can be shown by verification and Web service compositions can be modeled intuitively. In order to show the framework’s principle applicability, an example approach is analyzed with respect to the corresponding requirements.
Tài liệu tham khảo
Alonso G, Casati F, Harumi K, Machiraju V (2004) Web services. Concepts, architectures, applications. Springer, Heidelberg
Alves A, Arkin A, Askary S, Barreto C, Bloch B, Curbera F, Ford M, Goland Y, Guízar A, Kartha N, Liu C, Khalaf R, König D, Marin M, Mehta V, Thatte S, van der Rjin D, Yendluri P, Yiu A (2007) Web Services Business Process Execution Language. Version 2.0. http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html. Accessed 2008-12-29
Andrews T, Curbera F, Dholakia H, Goland Y, Klein J, Leymann F, Liu K, Roller D, Smith D, Thatte S, Trickovic I, Weerawarana S (2003) Business Process Execution Language for Web Services. Version 1.1. http://download.boulder.ibm.com/ibmdl/pub/software/dw/specs/ws-bpel/ws-bpel.pdf. Accessed 2008-12-29
Arjansani A (2004) Service-oriented modeling and architecture. How to identify, specify, and realize services for your SOA. http://www.ibm.com/developerworks/library/ws-soa-design1/. Accessed 2008-12-29
Arkin A, Askary S, Fordin S, Jekeli W, Kawaguchi K, Orchard D, Pogliani S, Riemer K, Struble S, Takacsi-Nagy P, Trickovic I, Zimek S (2002) Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/2002/NOTE-wsci-20020808. Accessed 2008-12-29
Balzert H (1998) Lehrbuch der Software-Technik. Software-Management, Software-Qualitätssicherung, Unternehmensmodellierung. Spektrum, Heidelberg
Bell M (2008) Service-oriented modeling. Service analysis, design, and architecture. Wiley, Hoboken
Booth D, Haas H, McCabe F, Newcomer E, Champion M, Ferris C, Orchard D (2004) Web services architecture. http://www.w3.org/TR/ws-arch/. Accessed 2008-12-29
Christensen E, Curbera F, Meredith G, Weerawarana S (2001) Web Services Description Language (WSDL) 1.1. http://www.w3.org/TR/2001/NOTE-wsdl-20010315. Accessed 2008-12-29
Clark J, DeRose S (1999) XML Path Language (XPath). http://www.w3.org/TR/1999/REC-xpath-19991116. Accessed 2008-12-29
Clarke EM, Grumberg O, Peled DA (2001) Model checking, 3rd edn. MIT Press, Cambridge
Dostal W, Jeckle M, Melzer I, Zengler B (2005) Serviceorientierte Architekturen mit Web Services. Elsevier Spektrum Akademischer Verlag
Dubray J (2008) BPML. http://www.ebpml.org/bpml.htm. Accessed 2008-12-29
Erl T (2004) Service-oriented architecture – A field guide to integrating XML and web services. Prentice Hall PTR, Upper Saddle River
Fahland D, Reisig W (2005) ASM-based semantics for BPEL: The negative control flow. In: Borger E, Beauquier D, Slissenko A (eds) Proceedings 12th international workshop on abstract state machines, Paris
Farahbod R, Glässer U, Vajihollahi M (2005) A formal semantics for the Business Process Execution Language for Web Services. In: Joint workshop on web services and model-driven enterprise information systems, Miami
Farahbod R, Glässer U, Vajohollahi M (2004) Specification and validation of the Business Process Execution Language for Web Services. In: Zimmermann W, Thalheim B (eds) Abstract state machines. Springer, pp 79–94
Ferrara A (2004) Web Services: A process algebra approach. In: Proceedings 2nd international conference on service oriented computing, New York
Ferstl OK, Sinz EJ (2006) Grundlagen der Wirtschaftsinformatik, 5th edn
Floyd RW (1967) Assigning meaning to programs. In: Proceedings 19th American Mathematical Society symposium in applied mathematics, Providence
Fu X, Bultan T, Su J (2004a) Analysis of interacting BPEL web services. In: 13th International WWW conference, New York
Fu X, Bultan T, Su J (2004b) WSAT: A tool for formal analysis of web services. In: 16th international conference of computer aided verification, Boston
Fu X, Bultan T, Su J (2005) Synchronizability of conversations among web services. IEEE Transactions on Software Engineering 31(12):1042–1055
Fu X, Bultan T, Su J (2006) Analyzing the conversations of web services. IEEE Internet Computing 10(1):18–25
Herman I (2003) Introduction to the semantic web. http://www.w3.org/2003/Talks/0624-BrusselsSW-IH/. Accessed 2008-12-29
Hevner AR, March ST, Park J, Ram S (2004) Design science in information systems research. MIS Quarterly 28(1):75–105
Hoare CAR (1969) An axiomatic basis for computer programming. Communications of the ACM 12(10):576–583
Holzmann GJ (2003) The SPIN model checker. Primer and reference manual. Addison Wesley, Boston
Kallus M (2004) Web Services vor dem Durchbruch. http://www.cio.de/news/802604/index1.html. Accessed 2008-12-29
Kavantzas N, Burdett D, Ritzinger G, Fletcher T, Lafon Y, Barreto C (2005) Web Services Choreography Description Language. Version 1.0. http://www.w3.org/TR/ws-cdl-10/. Accessed 2008-12-29
Klyne G, Carroll J (2004) Resource Description Framework (RDF). Concepts and abstract syntax. http://www.w3.org/TR/2004/REC-rdf-concepts-20040210. Accessed 2008-12-29
Kopp O, Frenkler C, Lohmann N (2006) Korrektheit und Zuverlässigkeit zusammengesetzter Web Services am Beispiel der Geschäftsprozess-Modellierungssprache BPEL. ftp://ftp.informatik.uni-stuttgart.de/pub/library/ncstrl.ustuttgart_fi/INPROC-2006–67/INPROC-2006–67.pdf. Accessed 2008-12-29
Lee K, Jeon J, Lee W, Jeong S, Park S (2003) QoS for web services. Requirements and possible approaches. http://www.w3c.or.kr/kr-office/TR/2003/ws-qos/. Accessed 2008-12-29
Lohmann N (2007) A feature-complete Petri net semantics for WS-BPEL 2.0. In: van Hee K, Reisig W, Wolf K (eds) Proceedings of the workshop on formal approaches to business processes and web services, Podlasie
Martens A (2005) Analyzing web service based business processes. In: Cerioli M (ed) Proceedings 8th international conference on fundamental approaches to software engineering
Martin D, Burstein M, Hobbs J, Lassila O, McDermott D, McIlraith S, Narayanan S, Paolucci M, Parsia B, Payne T, Sirin E, Srinivasan N, Sycara K (2004) OWL-S: Semantic markup for web services. http://www.w3.org/Submission/OWL-S/. Accessed 2008-12-29
Mitra N (2003) SOAP version 1.2 Part 0: Primer. http://www.w3.org/TR/2003/REC-soap12-part0–20030624/. Accessed 2008-12-29
Moser S, Martens A, Görlach K, Amme W, Godlinski A (2007) Advanced verification of distributed WS-BPEL business processes incorporating CSSA-based data flow analysis. In: Proceedings of the IEEE international conference on services computing, Salt Lake City
Newcomer E, Lomow G (2005) Understanding service-oriented architecture with web services. Addison Wesley Longman, Amsterdam
Papazoglou MP, van den Heuvel W (2006) Service-oriented design and development methodology. International Journal of Web Engineering and Technology 2(4):412–442
Peltz C (2003) Web services orchestration and choreography. Computer 36(10):46–52
Rozinat A, van der Aalst WMP (2008) Conformance checking of processes based on monitoring real behavior. Information Systems 33(1):64–95
Schlingloff H, Martens A, Schmidt K (2005) Modeling and model checking web services. In: Electronic lecture notes in computer science: Issue on logics and communication in multi-agent systems, Berlin
Schneider K (2004) Verification of reactive systems. Formal methods and algorithms. Springer, Heidelberg
Sommerville I (2004) Software engineering, 7th edn. Addison Wesley, Boston
Stahl C (2005) A Petri net semantics for BPEL. http://www2.informatik.hu-berlin.de/Institut/struktur/systemanalyse/preprint/stahl188.pdf. Access 2008-12-29
van Breugel F, Koshkina M (2006) Models and verification of BPEL. http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf. Accessed 2008-12-29
Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: First symposium on logic in computer sciences, Cambridge
Wilde T, Hess T (2007) Forschungsmethoden der Wirtschaftsinformatik – Eine empirische Untersuchung. WIRTSCHAFTSINFORMATIK 49(4):280–287
Zimmermann O, Krogdahl P, Gee C (2004) Elements of service-oriented analysis and design. An interdisciplinary modeling approach for SOA projects. http://www.ibm.com/developerworks/library/ws-soad1/. Accessed 2008-12-29