An ECLIPSE Plug-In for Formal Verification of BPMN Processes

The Business Process concept represents an important view in the Informative Systems in different application domains. Tools and modeling languages can be used by domain experts to contribute in the Business Process design of the systems. In most of the cases, specifications of Business Process is done without a formal semantic. Resulting systems do not match functional and non-functional requirements due to the communication problems between domain experts and IT-developers. To solve such issues we propose a novel approach enriching the design with a formal semantic and a systematic integration of formal verification. The approach has been implemented as user friendly tool able to design and verify Business Process. The tool is an ECLIPSE plug-in that uses BPMN notation for Business Process specification, implements a mapping from BPMN to the CSP formal language and supports CSP verification via model checking. It is named BP4PA. The proposed approach and tool have been applied on real scenarios.