VERBUS: A formal model for business process verification

Business process management is a key issue in B2B. Different process modelling languages and workflow management tools and frameworks have appeared to aid the development, deployment and management of e-commerce solutions. Nevertheless, there is not yet a framework to compel with tasks such as guaranteeing: safety outcomes of the run of a composition of processes, the eventual execution of processes under some condition, or the soundness of a design with respect to the specification. This is the mission of format methods. and they have been successfully applied in the fields of real-time software, hardware verification, and a growing list of application areas as the computation costs decrease. In this article we present VERBUS, a formal system for the modelling and verification of business processes. VERBUS allows a designer to specify properties for verification. The Finite State Machine theory is under the hood of VERBUS, providing the designer with a well-known and understandable approach, which offers a set of existing tools for verification or for compiling to other formats for the application of model-checkers.