BPEL checker

Eclipse plugin

Download

External dependecies

Publications

Overview

BPEL checker is a command-line tool for verification of BPEL code against session protocols. For a given web service implemented in the BPEL language (a BPEL script), the tool can check whether the BPEL script interacts with other services according to the constraints on the order of operation invocations of the other services – the constraints being expressed via session protocols that are defined in the formalism of behavior protocols.

Session protocol for a particular web service is stored in a BPEL script inside the custom sessionProtocol sub-element of the partnerLink element that identifies a service the BPEL script interacts with.

The verification process involves translation of a BPEL script into a Java program (via a modified version of the B2J tool) and checking of the generated Java program against behavior protocols via combination of the Java PathFinder model checker and Behavior Protocol Checker.

As an input, the tool accepts the name of the BPEL source file and the path to a directory for generated Java files. The output includes a short report on checking result and, if the BPEL script interacts with one of the services in an incorrect way, an error trace.

Usage of the tool is illustrated by a simple demo that involves a BPEL script interacting with two other services. Two versions of tbe BPEL script are provided – a correct one (AirlineCustomerOk.bpel) and one that uses the other services in an incorrect way (AirlineCustomerBad.bpel).

The BPEL checker tool is developed and supported by Pavel Parizek.

Eclipse plugin

BPEL checker plugin for Eclipse allows checking of BPEL files in a simple way. The plugin publishes the Check BPEL file action in the context menu of the file navigator that is associated (and enabled) only for files with the bpel extension. When this action is executed, the BPEL checker is run and its output is displayed in the Eclipse console.

The BPEL checker Eclipce plugin is developed and supported by Michal Malohlava.

Screenshot

Download

  • BPEL checker
    • Binary (including modified B2J tool): zip, tgz
    • Source code (including modified sources of B2J): zip, tgz
    • Demo: zip, tgz
  • Eclipse plugin
    • Binary (including the BPEL checker): zip
    • Source code (Eclipse project): zip

External dependencies

Publications

2008 (2)

Refereed (journals/proceedings)

PDF, Link Parízek P., Adámek J.: Checking Session-Oriented Interactions between Web Services,
In Proceedings of 34th EUROMICRO SEAA conference, IEEE Computer Society, ISBN 978-0-7695-3276-9, pp. 3-10, September 2008

Technical Reports

PDF Parízek P., Adámek J.: Modeling and Verification of Session-Oriented Interactions between Web Services: Compliance of BPEL with Session Protocols,
Tech. Report No. 2008/2, Dep. of SW Engineering, Charles University in Prague, January 2008
Modified on 2010-11-02