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.
An ECLIPSE Plug-in for Formal Verification of BPMN Processes
Corradini Flavio;Polzonetti Alberto;Re Barbara;Falcioni Damiano
2010-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
