Towards a Full Model-Driven Approach for Modeling and Verifying Business Process Models Using CPN

1. Introduction

For software systems that support modern enterprise infrastructures, the importance of reliability and safety is increasing. In this context, formal methods which provide effective tools to guarantee the correctness of software from the early stages of programming improvement gives incredible consideration. The formal methods are mathematically unambiguous techniques for software and hardware system design, development, and verification.

In the modern enterprise, Software design specifications are currently described using diagrammatic notation (BPMN, UML…) which might have a lot of interpretations. Modeling languages for business processes were developed and are commonly used in the early phases of software design specifications. Most of them, however, such as pattern-based methods, lack proper formal semantics and therefore cannot be checked and analyzed. Formal methods are therefore crucial and imperative in software verification, especially for safety-critical systems where failures can lead to catastrophes such as death of people or high economic losses. Based on the above considerations, many researchers suggested mapping workflow patterns to formal methods to perform system verification and analysis.

Firstly, for several reasons, Petri Nets formalism is one of the most promising methods. In (Van der Aalst, 1998) at least three factors have been given: (i) Formal semantics considering the graphic nature, (ii) State-based rather than (just) event-based, and (iii) Availability of several empirical techniques. Nonetheless, using classical Petri Nets is difficult, if not impossible, to realize most workflow patterns. For example several patterns addressing multiple instances and advanced synchronization patterns. The use of high-level Petri nets such as Colored Petri Nets (CPN) (Jensen, 1997), (Jensen and Kristensen, 2015) and (Valero et al. 2015) is more suitable for these considerations.

In addition, the paper authors quoted in (Russell et al. 2006) have established at least 20 control flow patterns that can be expressed in Colored Petri Nets. However, like all Formal methods, Colored Petri nets have a systematic mathematical structure that is challenging and difficult for non-experts to grasp. The purpose of our research is to allow business process specialists to formally validate their process models without having a solid understanding of formal methods.

In this article, the authors design an automated framework for mapping business process models to their colored Petri Nets. Model- driven Engineering (MDE) (Schmidt, 2006) tends to be the right approach to use to address such needs because it is a new software engineering framework focused on models, meta-models, and model transformations. Therefore, MDE concepts will be applied to model and test the BP models via this research.

This paper focuses on the problems of modeling and analysis involved in defining the conceptual and syntactical consistency of business process requirements prior to implementation. More specifically, utilizing colored Petri Nets formalism, the authors suggest a method and a tool to promote modeling and testing of business process models. “CPN tools,” a high- Petri net tool for editing, simulating and analyzing colored Petri Nets, is used to support the analysis (CPN Tools). Here, the decision to use CPN is motivated by the existence of hierarchical colored Petri nets capable of modeling complex patterns of large business processes. Within the MDE paradigm and CPN tools, the authors suggest using the well-known multi-formalism and meta-modeling ATOM³ tool (De Lara and Vangheluwe, 2002) to realize our approach fully automated.

In this context, the authors propose a full Model-Driven approach for modeling and Verifying Business Process Models using graph grammar and Colored Petri Nets. It consists of four steps:

• •

  Meta-Modeling BP and Colored Petri formalisms;

• •

  Creating a Model-to-Model Transformation through the Graph Grammar “Gram BP2CPN” to convert BP models into their equivalent Colored Petri net models;

• •

  Creating a Model-to-Text Transformation through the Graph Grammar “Gram CPN2DTD” to reconstruct the resulting Colored Petri net models in the CPN tools XML format;

• •

  Performing a State Space Exploration and Verification of the CPN model obtained directly in CPN Tools,” a high- Petri net tool for editing, simulating and analyzing colored Petri Nets”.