Compositional execution semantics for business process verification

Emmanouela Stachtiari

doi:10.1016/j.jss.2017.11.003

Return

Compositional execution semantics for business process verification

2018-03-01

PRE

Emmanouela Stachtiari *

Panagiotis Katsaros

DOI：10.1016/j.jss.2017.11.003

Original

Original request for help

Save

Abstract

En 中文

Service compositions are programmed as executable business processes in languages like WS-BPEL (or BPEL in short). In such programs, activities are nested within concurrency, isolation, compensation and event handling constructs that cause an overwhelming number of execution paths. Program correctness has to be verified based on a formal definition of the language semantics. For BPEL, previous works have proposed execution semantics in formal languages amenable to model checking. Most of the times the service composition structure is not preserved in the formal model, which impedes tracing the verification findings in the original program. Here, we propose a compositional semantics and a structure preserving translator of BPEL programs onto the BIP component framework. In addition, we verify essential correctness properties that affect process responsiveness, and the compliance with partner services. The scalability of the proposed translation and analysis is demonstrated on BPEL programs of various sizes. Our compositional translation approach can be also applied to other executable languages with nesting syntax. (C) 2017 Published by Elsevier Inc.

Keywords:

Formal verification

Programming language semantics

WS-BPEL

BIP

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.