Naslov
Formal Checking of WS-BPEL Orchestrations

Autori
Matković, Jelena ; Fertalj, Krešimir

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
37th International Convention on Information and Communication Technology, Electronics and Microelectronics / Biljanović, Petar et.al. - Opatija : Hrvatska udruga za informacijsku i komunikacijsku tehnologiju, elektroniku i mikroelektroniku - MIPRO, 2014, 375-381

ISBN
978-953-233-078-6

Skup
37th International Convention on Information and Communication Technology, Electronics and Microelectronics

Mjesto i datum
Opatija, Hrvatska, 26.05.2014. - 30.05.2014

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
WS-BPEL Orchestrations

Sažetak
This paper is focused on understanding techniques used to formally verify behaviour of business processes developed using WS-BPEL standard. The first part of the paper gives an overview of WSBPEL control-flow constructs. We analyze offered constructs and try to derive control-flow scenarios that can be built out of them. Derived complex control- flow scenarios are further discussed. Possible execution misbehaviour, which cannot be discovered by pure static analysis of WSBPEL code, is identified. Misbehaviour can be any of the following: unreachable code, deadlock states, non-progress cycles (code is repeated without passing through progress state), or any other unwanted scenario, like unwanted execution order of activities, unwanted order of messages being exchanged and similar execution misbehaviour. The second part of the paper describes techniques used for formal verification of any code in general with an emphasis on research how these techniques are exploited to verify WS-BPEL code. The final part of the paper concludes with the discussion how successful described work was in verification of possible identified misbehaviour from the first part of the paper.

Izvorni jezik
Engleski

POVEZANOST RADA