Checking Session-Oriented Interactions between Web Services

0317131 - ÚI 2009 RIV US eng C - Konferenční příspěvek (zahraniční konf.)
Parízek, P. - Adámek, Jiří
Checking Session-Oriented Interactions between Web Services.
[Ověřování relačně-omezené komunikace mezi webovými službami.]
34th Euromicro Conference Software Engineering and Advanced Applications. Los Alamitos: IEEE Computer Society, 2008, s. 3-10. ISBN 978-0-7695-3276-9.
[SEAA 2008. EUROMICRO Conference on Software Engineering and Advanced Applications /34./. Parma (IT), 03.09.2008-05.09.2008]
Grant CEP: GA AV ČR 1ET400300504
Výzkumný záměr: CEZ:AV0Z10300504
Klíčová slova: web services * BPEL * session-oriented interactions * behavior protocols * model checking
Kód oboru RIV: JC - Počítačový hardware a software

Although web services are generally envisioned as being stateless, some of them are implicitly stateful, because web services often work as front-ends to enterprise systems and are used in a session-oriented way by the clients. Unlike stateless services, a stateful web service imposes constraints on the order in which the operations of the service may be invoked. However, specification of such constraints is not a standard part of a web service interface, and compliance with such constraints is not checked by the standard web service development tools. In this paper, we propose an extension to a web service interface consisting of a constraint definition based on behavior protocols. We also describe a tool that checks whether a given BPEL code complies with the constraints of all stateful web services it communicates with. The key idea behind the tool is to translate the BPEL code into Java and then to check the Java program using Java PathFinder with behavior protocol extension.

Přestože webové služby jsou obecně viděny jako bezstavové, některé z nich jsou implicitně stavové. Důvodem jě to, že webové služby často pracují jako front-end k podnikovým systémům a jsou používány jejich klienty relačním způsobem. Narozdíl od bezstavových služeb, pro stavovou službu existují omezení na pořadí, ve kterém operace dané služby mohou být volány. Nicméně, specifikace takových omezení není standardní součástí rozhraní webové služby, a korespondence s těmi omezeními není ověřována běžnými nástroji pro vývoj webových služeb. V tomto článku navrhujeme rozšířit rozhraní webových služeb pomocí definice omezení, která je založena na protokolech chování. Dále jsme implementovali nástroj pro ověřování, jestli BPEL kód splňuje omezení všech stavových webových služeb, se kterými komunikuje. Hlavní myšlenka je překlad BPEL kódu do jazyka Java a ověřování Java programu pomocí nástroje Java PathFinder s rozšířením pro protokoly chování.
Trvalý link: http://hdl.handle.net/11104/0166858