Home UC3M
Home IT
Home /Personnel /Assistants /Jesús Arias Fisteus /VERBUS

Verification for Business Processes


VERBUS (VERification for BUSiness processes) is a modular and extensible framework for automatic business process verification. It proposes an architecture with three layers: the design layer, the formal layer and the verification layer. The formal layer is a business process specification model based on FSMs formalism. It disconnects process description languages and verification languages. Process definitions (design layer) can be automatically translated to specifications in the formal layer. These specifications can be automatically translated to specifications in the verification layer and verified using verification tools.

The current prototype of VERBUS uses BPEL4WS as process definition language (design layer). It can generate Promela and SMV verifiable models. Promela models can be verified with Spin. SMV models can be verified with SMV or NuSMV.

Architecture of Verbus


The prototype of VERBUS is being developed in Java language as free software under the GNU GPL License. Development is managed through SourceForge. Visit the verbus project page at sourceforge.

You can download the source code from:

  • SourceForge CVS archive.
  • Latest alpha release (version 0.1-alpha-7): verbus-src-0.1a7.tgz (it includes the required libraries).

Note that current version of this prototype is experimental and several required features have not been implemented yet. Some functionality may not work properly in this prototype. Want to collaborate? Contact Jesús Arias Fisteus.


This table shows some examples of automatic translations using VERBUS.

BPEL4WS spec. VERBUS formal spec. Promela model SMV model
olive.bpel, olive.wsdl olive.vbs olive.pml olive.smv
orders.bpel, orders.wsdl orders.vbs orders.pml orders.smv


Last update:

Location |Personnel |Teaching |Research |News |Intranet
home | site map | contact