Title: Automatic verification of business process integrity

Authors: Manuel I. Capel-Tunon, Luis E. Mendoza-Morales, Kawtar Benghazi-Akhlaki

Addresses: Dpto. de Lenguajes y Sistemas Informaticos, ETS Ingenierias Informatica y de Telecomunicacion, C/Periodista Daniel Saucedo Aranda s/n, Universidad de Granada, E-18071, Granada-Espana. ' Universidad Simon Bolivar, Dpto. de Procesos y Sistemas, Edif. Matematicas y Sistemas, piso 3, Valle de Sartenejas, Baruta, Edo. Miranda. Apartado 89000, Caracas 1080-A. Caracas – Venezuela. ' Dpto. de Lenguajes y Sistemas Informaticos, ETS Ingenierias Informatica y de Telecomunicacion, C/Periodista Daniel Saucedo Aranda s/n, Universidad de Granada, E-18071, Granada-Espana

Abstract: Software engineering methods have shown to be useful in Business Process Modelling (BPM) for improving business-modelling techniques. In this paper, we describe how a Model-Checking (MC) verification technique for software can be integrated with a formal-oriented software design method named MEDISTAM-RT. This is currently used in the development of the Task Model (TM) associated with a Business Process (BP) definition by using UML, enriched with temporal annotations in CSP + T, as the main modelling language. To show a practical use of our proposal, an example of a BPM enterprise-project related to the Customer Relationship Management (CRM) business is discussed.

Keywords: business process modelling; model checking verification; formal methods; software design; software engineering; task model; customer relationship management; CRM; business process integrity.

DOI: 10.1504/IJSPM.2008.023679

International Journal of Simulation and Process Modelling, 2008 Vol.4 No.3/4, pp.167 - 182

Published online: 07 Mar 2009 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article