A business process is a complex web service with functions provided by different web services, which are already existing in web and are dynamically integrated for granting a more complex business task. For this reason, business processes have become more and more diffuse in B2B and B2C domains, so that the importance of their activities asks for a high-level of reliability. Methods and tools for supporting automatic system verification and validation could be useful. Among the techniques of automatic verification, we choose Model Checking method, because we applied it efficiently for verification of a single web service and in this paper we extend the area of application also in business processes. Descriptions of the behavior of a business process are coded using a standard language, BPEL4WS, that has broadly spread because it is able to describe a business process as both an executable process and an abstract process. Therefore, we model a BPEL description of a generic business process with a formal model and we formalize correctness properties about the reliability of the business process design. Also, we build a framework that performs automatic verification of formal models of business processes through NuSMV model checker If there is a violation of correctness specifications, NuSMV provides counter-examples, so we can locate errors and effect right changes for correcting business process design.

Modelling and verification of BPEL business processes / Mongiello, Marina; Castelluccia, Daniela. - STAMPA. - (2006), pp. 144-148. (Intervento presentato al convegno Model-based Methodologies for Pervasive and Embedded Software, MBD/MOMPES 2006 tenutosi a Potsdam, Germany nel March 30, 2006) [10.1109/MBD-MOMPES.2006.22].

Modelling and verification of BPEL business processes

Mongiello, Marina;
2006-01-01

Abstract

A business process is a complex web service with functions provided by different web services, which are already existing in web and are dynamically integrated for granting a more complex business task. For this reason, business processes have become more and more diffuse in B2B and B2C domains, so that the importance of their activities asks for a high-level of reliability. Methods and tools for supporting automatic system verification and validation could be useful. Among the techniques of automatic verification, we choose Model Checking method, because we applied it efficiently for verification of a single web service and in this paper we extend the area of application also in business processes. Descriptions of the behavior of a business process are coded using a standard language, BPEL4WS, that has broadly spread because it is able to describe a business process as both an executable process and an abstract process. Therefore, we model a BPEL description of a generic business process with a formal model and we formalize correctness properties about the reliability of the business process design. Also, we build a framework that performs automatic verification of formal models of business processes through NuSMV model checker If there is a violation of correctness specifications, NuSMV provides counter-examples, so we can locate errors and effect right changes for correcting business process design.
2006
Model-based Methodologies for Pervasive and Embedded Software, MBD/MOMPES 2006
0-7695-2538-5
Modelling and verification of BPEL business processes / Mongiello, Marina; Castelluccia, Daniela. - STAMPA. - (2006), pp. 144-148. (Intervento presentato al convegno Model-based Methodologies for Pervasive and Embedded Software, MBD/MOMPES 2006 tenutosi a Potsdam, Germany nel March 30, 2006) [10.1109/MBD-MOMPES.2006.22].
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/11589/23036
Citazioni
  • Scopus 30
  • ???jsp.display-item.citation.isi??? 15
social impact