Service Verification

We aim at the verification of distributed business processes.

The idea is to provide business analysts, service designers, and programmers with tools that allow for detecting problems at design time. The designer implements its own process in a suitable language, e.g., Concrete BPEL4WS. This process interacts with external and available processes, e.g., abstract BPEL4WS that specify the interactions with other processes. Given the concrete internal process, the abstract external processes that have been published and that can be downloaded, and a set of business requirements, the WS-VER tool allows to check whether the requirements are violated. If this is the case, an "error flow", i.e., a flow of interaction that causes the problem is reported to the developer that can modify the BPEL4WS process and re-iterate the verification step.

We use formal analysis techniques, in particular Symbolic Model Checking, to pinpoint problems and to identify possible solutions.

Some relevant publications: