BPMN is a visual notation for modeling business processes. Although there are many tools supporting it, they rarely provide formal verification of models. We propose a new approach to formal verification of BPMN models using the Alvis modeling language and the XTT2 knowledge representation. The structure of the BPMN model can be analyzed using translation to Alvis. Alvis models can be verified with dedicated tools, and their properties can be linked to the properties of the original BPMN model. On the other hand, selected BPMN elements can be verified using the XTT2 decision tables. Several BPMN elements can be translated to XTT2 and checked using the HeaRT rule engine with the HalVA verification and analysis tool. The paper constitutes an overview of the methods and concepts and presents preliminary results of our research.
Business Process Model and Notation (BPMN) has recently emerged as a leading visual notation for modeling Business Processes. A BPMN model defines how the organization works by describing the ways in which operations are carried out to accomplish its intended goals. The progress in using the BPMN notation and the increasing complexity of the modeled processes make new advanced methods and tools needed.
BPMN provides a large collection of notation elements and allows for modeling various workflow structures, such as conditional operations, loops, event-triggered actions, splits and joins of sequence flow, etc. Moreover, it supports the hierarchical approach to design; thus, the process can be modeled on several abstraction levels.
The complexity of BPMN makes the formal verification of models a tough task.
Although there are many tools supporting BPMN modeling, most of them do not provide
any kind of formal model verification. In this paper, a new hybrid approach to formal
verification of BPMN models is presented. It uses Alvis [
This hierarchical separation provides verification of distinct properties on different
abstraction levels. For the global (process structure) verification, the translation to Alvis
modeling language is considered. The structure of the BPMN model can be analyzed
thanks to its similarity to Alvis model, which is suitable for information systems
modeling with subsystems working in parallel. For the local (model elements) verification,
verification of single BPMN elements is considered. Such BPMN elements are mapped
to the XTT2 knowledge representation, which can be verified using the HeaRT rule
engine [
This paper constitutes an overview of the methods and concepts, and presents preliminary results of the research aiming at formal verification of selected BPMN models using Alvis and XTT2 methods. We have limited the presentation to describing a simple yet illustrative case study of a student’s project evaluation process.
The rest of the paper is organized as follows. Section 2 presents the BPMN notation and the selected case study. In Section 3 several works related to our research are presented. The BPMN model structure verification concept is introduced in Section 4, while the BPMN elements verification concept is given in Section 5. The evaluation of our approach is presented in Section 6. A short summary is given in the final section. 2
A Business Process can be defined as a collection of related tasks that produce a specific service or product for a particular customer. Business Process Model and Notation (BPMN) is a leading visual notation for modeling Business Processes. It uses a set of predefined graphical elements to depict a process and how it is performed. The current version of BPMN defines three models to cover various aspects of processes: 1. Process Model – describes the ways in which operations are carried out to accomplish the intended objectives of an organization. The process can be modeled on different abstraction levels: public (collaborative Business 2 Business Processes) or private (internal Business Processes). 2. Choreography Model – defines expected behavior between interacting business participants in the process. 3. Collaboration Model – can include Processes and/or Choreographies, and provides a Conversation view (which specifies the logical relation of message exchanges).
In our research, the internal Business Process Model is considered. There are four basic categories of elements used to model such processes: flow objects (activities, gateways, and events), connecting objects (sequence flows, message flows, and associations), swimlanes, and artifacts.
For the purpose of our research, only a subset of BPMN elements (flow objects and sequence flows) is considered. A task is a kind of activity, and a model defines the ways in which individual tasks are carried out. Gateways determine forking and merging of the sequence flow between tasks in a process, depending on some conditions. Events denote something that happens in the process. The icon in the event circle depicts the event type, e.g. envelope for message event, clock for time event (see Fig. 1).
Let us analyze an exemplary BPMN model of a simple student’s project evaluation
process. Fig. 1 depicts the evaluation process of a student’s project for an Internet
technologies course. However, the process can be used for any kind of a project depending
on the ruleTistlewShupipcrhessaerdeDaueptpolEixecdesstiovetLheengptharticular tasks [
Request for completing project Evaluation of a student’s work
Expecting for the completed
project
waiting
time
expired
the
completed
project
reveived
In theucsoednstoiddeefirende tehxeabmehpavlieo,rtohfeinpdrivoicdueaslsaigsenatps.pElaiechdatgoentthies describe wpitrhoajepcietceevaluation.
website
of source code implemented in Alvis Code Language (AlvisCL) [
If the apcroonjceucrtresnytonrtadxistriisbuctoedrrseycstte,mp.rPealsismivienaagreyntcsodontneonttpecrhfoercmkainnyginidsivpideurafolarcm- ed. Then, if the protjiveictyt, bcuotnptraoivnidse eaxmpeecchtaendismelfeomrtehentmaurytual eHxcTluMsioLn atnadgsd,ataitsycnacnhrobneizaetivoanl.uated and X
The graphical layer (communication diagram) is used to define interconnections a grade can be given according to the rules defined by the teacher. On the (communication channels) among agents. A communication diagram is a hierarchoi-ther hand, if the projceacltgrcaophntwahinosseannoydessymnatya xreperrersoenrtobrotlhakciknsdssoofmageenbtass(iacctirveeqourirpeadssicveo)natnednt, it is requested topbaretscoof mthpelmetoeddel. fArofmtetrhreelcoweievrilnegvetl.hFerocmomuspelrestpeodinpt roof jveicewt,,tthhee swyshteomlelapyreorcess starts from the sisypnrteadxeficnhedecankdinognlyaggraaipnh.icHaloawndecvoedre, liafyethrsemcuostmbepldeetseigdnepdr.oAjelvcist pisrovniodetsraeceived on few different system layers. The most universal one is denote by α0 and makes Alvis time, the process is terminated (thus, the author of the
similar to other formal languages. The layer is based onpthreojfeoclltowdionegsasnsoumtgpteiotnas:credit).
The exeaacmh pacletivweailglenbtehuassaecdcefsosrtopirtessoewnntpartoiocenssoofr aonudrpreerfsoeramrscihtscstoantecmeernntisnags saoohnierarchical approach atos pfoosrsmiblael; vtheerisfichceadtuiloenr.fuWncetiodnisicsucsalsletdheafteexriesatcihngstarteelmaetendtawutoomrkasticbaellfyo; rienhand.
case of conflicts, agents priorities are taken under consideration.
Most of the recent approaches to analysis of the BPMN models consider a restricted
subset of BThPeMkeNy ceolnecmepetnotfsAilnvitsh[e1,m4]oidsealn. Tagheenytthfoatcduesnootnescahneycdkisintingguoifshseedlepcatretdofproperties
of the BP MtheNsymsteomdeulndtherrocoungshideitrsatitornanwsifthoramdeafitinoend itdoenatiftyorpmersailstlinagn ginutaimgee.. An Alvis
model is a system of agents that usually run concurrently, communicate one with
anIn [
Raedts et al. presented an approach transforming BPMN models to Petri nets, and Athlveisseusteos tthhreeemmCodRelLl2ayaerlsg:egbrarpahicicalla, ncgodueaganed. sTyhstiesmaolnloe.wTshefocrodveelraiyfiecraistion of the model usiunsgedthtoedmefiCneRthLe2bethoaovlisoerto.f Binedcivaiudusael tahgendtsi.sEcaocvheargeedntpisrodebslcermibehwaivtheatpoiebce manually identified in the BPMN model, this can slow the result interpretation process.
Dijkman et al. in [
Similar research conducted by Ou-Yang and Lin [
Another research direction concerns the translation of BPMN models to Yet Another
Workflow Language (YAWL) [
One of the recent paper in the field of BPMN model verification by Lam [
The main drawback of these solutions is that it is difficult to map the resulting model back to the BPMN one. Although the tools reveal some errors in the model after translation, it is hard to find the corresponding place in the BPMN model and fix them. 4
In this section, we present the concept of BPMN model structure (global) verification. For such a verification, the model structure is translated to the Alvis modeling language. 4.1
Alvis [
The key concept of Alvis is an agent, which denotes any distinguished part of the system with a defined identity persisting in time. An Alvis model is a system of agents that usually run concurrently, communicate one with another, compete for shared resources etc. The dependencies among agents are described with three model layers: graphical, code and system one.
The code layer defines the behavior of individual agents. Each agent is described with a piece of source code. Agents can be either active or passive. Active agents perform some activities and each of them can be treated as a thread of control in a concurrent or distributed system. Passive agents do not perform any individual activity, but provide a mechanism for the mutual exclusion and data synchronization.
The graphical layer (communication diagram) defines connections (communication channels) among agents. A communication diagram is a hierarchical graph with nodes representing agents or parts of the model from the lower level. The diagrams allow for combining sets of agents into modules, represented as hierarchical agents. Active and hierarchical agents are drawn as rounded boxes while passive ones as rectangles. An agent can communicate with other agents through ports, drawn as circles placed at the edges of the corresponding agents. Communication channels are depicted as lines (or broken lines) with arrowheads showing the direction of communication.
From the users point of view, the system layer is predefined and only graphical and code layers have to be designed. The system layer is strictly connected with the system architecture and the chosen operating system. Alvis provides a few different system layers. The most universal one is denoted by 0 and makes Alvis similar to other formal languages. The layer is based on the following assumptions: 1) each active agent has access to its own processor and performs its statements as soon as possible; 2) the scheduler function is called after each statement automatically; 3) in case of conflicts, agents priorities are taken under consideration (if two or more agents with the same highest priority compete for the same resources, the system works indeterministically). 4.2
To verify the properties of the structure of the whole BPMN model, the model has to be transformed into Alvis model. The transformation procedure starts with preparing the initial set of agents which correspond to activities in the BPMN model. In the second stage, the initial set of agents is optimized. An Alvis agent can work like a buffer which collects a signal/value and then sends it to the next agent.
For each identified agent, we define its interface (ports) by considering the set of surrounding edges for a given BPMN activity i.e. sequence flows that go to or from the activity; however, if a sequence flow goes from the activity to a gateway, we consider the sequence flow going from the gateway. Each surrounding edge is transformed into a port of the corresponding agent. Moreover, for each port an identifier (a name) has to be added. To complete the agent definition, its behavior should be defined with additional code in the Haskell functional programming language.
Other agents in the Alvis model can be defined in very similar way. Moreover, in the considered example, a student is treated as a part of the system environment in the Alvis model. Thus, a project (its submission or resubmission), a grade and a timeout are sent via border ports, which have to be further specified. To represent the possibility of a Title Suppressed Due to Excessive Length submit timeout, the agent definition should contain the Alvis statement with a time out branch. After receiving an error signal, the agent waits particular time for a revised project, and
Syntax after this timegeat time_oeurrtosrignal is generavtaeliddatiaonnd the agent finishes its activity.
Although in APlCvCis a decision table activity can be represented as Haskell function, such an approach is bepyasosnedd the scope of this paper. The approach considering full Alvis representation of the presented BPMN model was proposed in [4R]e.queIsntfotrhe approach presented in this paper, Alvis is used only assynataxteorroorl for global vecormipfilectinagtion. For the project purpose of local verification, the XTT2 method suits much better, and contrary to Alvis missing can provide a precise verification of singpalsesedBPMN eblaesimcents, such as gateways or tasks.
The last stage of the transformation procedure iscotnotentdefine communication channels in the Alvis model graphical layer, whicPhrceloiinmnteinnamtry ost cases consist in connecting pairs of ports. A more complex case is the transfocrhmeckaintgion of the OR gateway, which requires to connect twFoig.p1a.4irGsenoefraptioonrotfsc.oTmmheuniccoatmionpclheantenelcsommunication diagram is shown in Fig. 2. submit passed get
SV PCC get error error passed project
resubmit
ECP error
time_out
ESW get grade verification of the model. Next, the Alvis model is transformed into a labelled transition system (LTS), used for formal verification. An LTS graph is an ordered graph with nodes denoting states of the considered system and edges denoting transitions among states. A state of a model is represented as a sequence of agents states. A state of an agent is four-tuple that consists of: agent mode (e.g. running, waiting), its program counter (point out the current step/statement), context information list (contains additional information e.g. the name of called procedure) and a tuple with parameters values.
There are two possible approaches to the formal verification of an LTS graph. If the graph is stored in the form of Haskell list, it is possible to add additional functions that inspect the list e.g. to find states with specified properties. On the other hand, such an LTS graph can be encoded using the Binary Coded Graphs (BCG) format and verified with the CADP toolbox.CADP offers a wide set of functionalities, ranging from stepby-step simulation to massively parallel model-checking. The verified properties can be divided into two groups usually called safeness and liveness ones. The former link with states properties while the latter link with an LTS graph paths’ properties.
Apart from the BPMN model structure analysis, checking several properties of single
BPMN elements (local verification) is needed. Thus, our approach allows for
verification of selected BPMN elements, which are mapped to the XTT2 knowledge
representation. Thanks to the formal representation of XTT2, it is possible to verify several
properties of these elements using the HeaRT rule engine [
EXtended Tabular Trees v2 (XTT2) is a knowledge representation that incorporates
an attributive table format. In this approach, similar rules are grouped in separated
tables, and the system is split into a network of such tables representing the inference
flow [
Several problems related to selected BPMN elements may be considered. In the case
of gateways, it should be checked if all the possible conditions are taken into account
during the design. The proposed approach is as follows. A gateway BPMN element is
translated to a table XTT2 knowledge representation – in this case it is represented as
a single table. Diagram elements are translated to the XTT2 form according to
appropriate logic functions. Thus, a BPMN element and its sequence flows are transformed
to an XTT2 table filled with proper rules. Similar approach to the analysis of the BPMN
elements and corresponding logic functions can be found in [
An exemplary decision table corresponding to the XOR gateway from the case study is presented in Fig. 3. The table consist of four columns. The first two, marked with (?), contain condition attributes, and the second two, marked with (->), contain the decision attributes. Each row contains a single rule that specifies the requirements for the flow.
The syntax of the resulting table can be validated in HQEd and then verified using HeaRT with HalVA. In the presented example, assuming that the validation attribute can take one of three values: error, passed or warning, the table can be verified against its completeness. It can be observed that the state in which the validation attribute takes the warning value is not included.
It is important to note that even if all model elements are validated, the whole model structure is still not grasped. Therefore, the verification of the model structure, presented in Section 4, is needed. syntax = checked validation = passed validation = error (?) syntax (?) validation (->) error flow (->) passed flow checked checked error passed Since BPMN does not specify the control logic of particular tasks, currently it has to be implemented manually. In the proposed approach it can be specified either using rules in the form of the XTT2 table or network, or as a HeaRT callback.
After specification of the task logic using the XTT2 decision tables, there is a
possibility of their formal verification. Currently, HeaRT with the HalVA module allows for
verification and analysis of the XTT2 table, i.e.: checking the inconsistency of a single
rule, inconsistency of a pair of rules, incompleteness (lack of the ability to react for
every admissible input values), subsumption of conditions and subsumption of a pair of
rules, as well as identity and equivalence of rules [
An exemplary XTT2 decision table for the Evaluation of a student work task is shown in Table 1. The table can be used for evaluation a project, according to the specified rules. The output of the table is a grade for a project.
(?) implemented functionality (?) quality (->) grade = basic = any = basic = advanced = advanced = low := satisfactory (D) = low := satisfactory (D) = high := good (C) = fair := very good (B) = high := excellent (A)
Table 1. Decision table for student’s project evaluation
In the presented table, it can be observed that there is no rule which can determine the grade when implemented functionality is basic and the quality of the project is fair. Thus, the verification would give the information about uncovered states (incompleteness), as well as it would inform that the second rule subsumes the first one. This is important when the system has to work correctly for any admissible input data and produce deterministic, consistent solutions.
The verification method presented in this paper is a new hybrid approach to the BPMN model verification and constitute a preliminary attempt to BPMN model execution.
From the structure point of view, the Alvis model resembles the original BPMN
one. After a verification of the Alvis model, it is easy to link the model properties to the
properties of original BPMN model. Contrary to the solutions presented in [
From the single element point of view, the approach allows for using rule verification methods. Although this requires to specify gateway conditions using the ALSV(FD) logic and define the logic of tasks using the XTT2 representation, this can be a consistent method, complementary to the Business Processes. Moreover, the transformation from BPMN to XTT2 can be used for execution purposes in the future.
Therefore, the presented approach differs from the earlier attempts in addressing hierarchical verification of BPMN models. It allows for verification of both: 1. model structure (or flow) and 2. single elements (gateways and tasks) of the BPMN model.
In both presented cases, the BPMN elements are taken into account. However, thanks to the separation of layers, the approach provides the verification of distinct properties on different abstraction levels.
In the case of the BPMN model structure, the properties to verify can be divided into two groups: safeness and liveness. The former is related to states properties e.g. a project with correct content cannot be treated as a defective one. The latter concerns properties of LTS graph paths e.g. if the time out signal has not been generated and a project with correct content has been provide, the system must provide a suitable grade.
When it comes to the BPMN elements, there are many properties which can be verified, such as: lack of redundancy, consistency, minimal representation, or completeness.
Although the approach concerns only a small subset of BPMN, extending of this subset is expected in the future. Dedicated tools enabling automatic translation of the BPMN model to Alvis and XTT2 representations are planned to be implemented. Moreover, the formal definition of transformation rules will be developed. 7
The paper presents preliminary results of the research concerning verification of BPMN models. The original contribution is the proposal of a hybrid and hierarchical approach to formal verification of selected BPMN models. We propose an approach which uses the Alvis modeling language for the global verification of the model structure and the XTT2 knowledge representation for the local verification i.e. verification of single BPMN elements in the model. The presentation of the approach has been limited to the presentation of a simple, yet illustrative, case study of a student’s project evaluation process. The considered example contains only a few activities, gateways, and events, However, it is possible to use the presented approach for more complex models.