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.
2010
9780769540702
273
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11581/229270
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact