Abstrakt
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í.