=Paper=
{{Paper
|id=Vol-2245/modevva_paper_1
|storemode=property
|title=ProVer: An SMT-based Approach for Process Verification
|pdfUrl=https://ceur-ws.org/Vol-2245/modevva_paper_1.pdf
|volume=Vol-2245
|authors=Souheib Baarir,Reda Bendraou,Hakan Metin,Yoann Laurent
|dblpUrl=https://dblp.org/rec/conf/models/BaarirBML18
}}
==ProVer: An SMT-based Approach for Process Verification==
https://ceur-ws.org/Vol-2245/modevva_paper_1.pdf
ProVer: An SMT-based Approach for Process Verification
Souheib Baarir1, Reda Bendraou1, Hakan Metin1, Yoann Laurent2
1
Laboratoire d'Informatique de Paris 6, Paris, France
FirstName.LastName@lip6.fr
2 IQVIA, laurent.yoann@gmail.com
Abstract Inconsistencies can range from very basic syntactical
errors, to more complex issues such as deadlocks, inconsistent
Business processes are used to represent the enterprise’s allocation of resources and time on process’s activities or any
business and services it delivers. They are also used as a proprietary business constraints that might be violated by
means to enforce customer’s satisfaction and to create an potential process executions.
added value to the company. It is then more than critical to
seriously consider the design of such processes and to make Some process models, depending on the business domain (ex.
sure that they are free of any kind of inconsistencies. Healthcare or military), can be very complex and may contain
more than 250 activities with very sophisticated control and
This paper highlights the issues with current approaches data flows, resource and time constraints [Christov
for process verification and proposes a new approach called 14][Simidchieva 10]. Trying to analyze these processes and
ProVer. Three important design decisions will be motivated: to verify them without the help of a tool would be
1) the use of UML AD as a process modeling language, 2) the unmanageable. In [Mendling 09], a study demonstrated that
formalization of the UML AD concepts for process over 2000 inspected process models, 10% of these models
verification as well as a well-identified set of properties in where unsound. An equivalent study on SAP repository
first-order logic (FOL) and 3) the use of SMT (Satisfiability containing more than 600 complex process models
Modulo Theories) as a mean to verify properties spanning demonstrated that more than 20% had flaws. [Mendling 06,
different process’s perspectives in a very optimal way. The 07]. Similarly, Gruhn et al. [Gruhn 07] collected 285 EPC
originality of ProVer is the ability for non-experts to express (Even-Driven Process Chains) from different sources i.e.,
properties on processes than span the control, data, time, and repositories, scientific papers, thesis, etc., and came to the
resource perspectives using the same tool. conclusion that even though process models were
syntactically correct, more than 38% of them were unsound.
Introduction Finally, Vanhatalo et al. [Vanhatalo 07] analyzed more than
Processes, whatever the field (ex. software, military or 340 Business process models with a focus and the control
healthcare), are everywhere. They represent the building flow aspect to realize that half of them were invalid i.e.,
block of any information system nowadays. Business contained deadlocks or unreachable activities.
processes are used to represent the enterprise’s business and More than 20 years after the introduction of business
services it delivers. They are also used as a mean to enforce processes, it is quite surprising to realize that, despite the
customer’s satisfaction and to create an added value to the different approaches and tools provided by the literature for
company. Software processes are critical as well since they model verification, such ratio of errors still persist in the
represent the guaranty to respect development process’s domain of process models. One possible reason could be the
deadlines and to ensure a certain quality of the delivered complexity of some process models and the fact that they
software, which in some cases will end up being the integrate different perspectives and properties that need to be
company’s information system itself. It is then more than checked, each one requiring a specific tool or approach to
critical to seriously consider the design of such processes and validate it [Gruhn 06].
to make sure that they are free of any kind of inconsistencies.
In the following we give a motivating example to explain
our point.
Figure 1. The ProcessOrder business process example extracted from the UML Specification.
Motivating Example. Process models are mainly driven process model [Peterson 81]. However, verifying the property
by three perspectives: Control flow, Data flow and Resources. “is the invoice always produced after the execution of the Fill
In addition, more complexity can be introduced by other Order action?” (cf. Figure 1), implies using data from the
constraints related to the “Time” perspective as well as to system domain and imposes to use Colored Petri Nets
some project’s specific business constraints (ex. some (CPN)[Jensen 87]. Even if Petri nets, with their different
resources can be substitutable under some circumstances, variants, can represent anything defined in terms of an
some activities can be skipped under some conditions, etc.). algorithm, this does not imply that the modeling effort is
Figure 1 presents an example which highlights process acceptable. Hofstede's and Wohed’s paper [Hofstede 02]
perspectives. The notation used is UML Activity diagrams. gives concrete examples of some Workflow Patterns that need
The goal of this process is to manage the reception, very complex Petri nets extensions and tricks to represent
processing, payment and shipping of customers’ orders. The them while this is expressed very naturally in UML Activity
process contains 7 actions connected to control nodes diagrams (AD) [Wohed 05] or Business Process Modeling
(DecisionNode, ForkNode…) and represents the control flow Notation (BPMN) [OMG 11] which are among the modeling
perspective. The data perspective is represented through the languages that support most of the workflow patterns as
so-called input/output Pins (see notation details in the figure). demonstrated in [Van der Aalst 03]. When it comes to the
They represent what an action might require to trigger its properties to be checked on process models, most of the
execution or what it might produce as the result of its approaches focus on the control flow aspect [Van der Aalst
execution. Some organizational aspects/constraints are 11b], only a few of them address the data perspective [Awad
annotated on the diagram such as the resources used by 09, Trcka 09, Knuplesch 10] or the time perspective [Eshuis
actions (ex. BankConnector) and time constraints on top of 02, Guelfi 05, Watahiki 11]. No approach proposes to address
each action in terms of hours. Time units could also be used all these perspectives in a unified way. For instance, in the
instead. process depicted in figure 1, expressing a property such as “is
it possible to reach the end of the process in less than 8 hours
One way to validate such process models is to use formal while making sure that the invoice artifact is produced and
verification techniques such as Model-Checking. In the field without using the BankConnector resource?” would be
of business processes many approaches have been proposed challenging.
for process verification [Eshuis 06, Wong 07, Liu 07, Trck 09,
Fahland 09, Van der Aalst 11]. They address essentially what Another obstacle for the limited adoption of formal
it is called soundness properties [Van der Aalst 11]. These techniques and approaches for process model verification in
properties guarantee the absence of deadlocks, unreachable the industry comes from the process modelers’ resistance to
activities, and other anomalies that can be detected without express process constraints and properties using formal
domain knowledge. However none of these approaches was languages [Emerson 90, Smith 02, Keleppe 03, Awad 07 &
really adopted in the industry [Morimoto 08]. Their 08]. Due to the lack of mathematical background, properties
complexity, the requirement of a mathematical background to are usually expressed in natural language and then given to
use them and very often, a lack of a user-friendly tooling experts that will translate these properties into a mathematical
support was an obstacle for their adoption [Gruhn 06, formalism with the eventual risk of misinterpreting what was
Mendling 09]. But more specifically, let’s illustrate what we initially required by the process modeler [Smith 02]. Other
believe to be an issue in the current approaches and the process modelers would prefer going through the process
problems we intended to contribute to with our work. In the model and double checking it or by adding some exception
following we categorize the different issues we identified handlers in the process model and extra checks in order to
after a review of the state of the art in the domain of software make sure that the process is sound. Of course, this is not
and business process verification. A detailed review of the feasible in the case of complex and sophisticated process
different approaches (more than 23) is given in [Laurent 18] models. These will definitely need a Model-Checking tool to
ensure that the properties/constraints are satisfied whatever
Identified issues in process verification. A major the process execution. LTL (Linear Temporal Logic) [Pnueli
point with current process verification approaches is about the 77] or CTL (Computation Tree Logic)[Hafer 87] are usually
formalism and tools they rely on for performing the used to express these properties.
verification. Whatever the process modeling language (PML),
a formal semantics is given to the language by mapping its Finally, current approaches and Model-Checking tools
constructs to either variants of automata [Guelfi 05, Eshuis are not fully integrated to process modeling tools and the
06], Petri nets [Van der Aalst 98 & 11, Trcka 09, Fahland 09, verification workflow is not always fully automated. Some
Jung 10] or process algebra [Wong 07, Liu 07]. However, this translation steps of the process models and of the properties to
means that we are relying on the semantics of the targeted be checked towards the verification formalism have to be
formal language concepts in terms of expressiveness, e.g. done manually in some approaches [Van der Aalst 99,
Petri Nets, instead of the modeling language itself. For Dijkman 08]. Moreover, usually the results of the verification
instance, if one wants to check the following in case of a counter-example is found is not explicitly
property/constraint: “is the Close Order action always reported graphically on the process model so that the process
executed?”, he can use classical Petri nets to represent the modeler can clearly identify the problem. Instead, the existing
approaches propose a list of states representing the process semantics of UML AD is given in natural language in the
execution that failed. standard specification which could be ambiguous and a source
of misinterpretations. However, the OMG (Object
In conclusion, the issues we identified during a thorough
Management Group) issued a new standard called fUML
study of the literature for process model verifications are: 1)
(Semantics of a Foundational Subset for Executable UML
the need to rely on the semantics of a target formal language
Models) that aims at giving a precise semantics to a subset of
which may limit the expressiveness of process models; 2) the
UML [OMG 11b]. The operational semantics of this subset
inability of current approaches to support the different process
are given in a pseudo java-code which is supposed to reduce
perspectives (control flow, data flow, time and resources) in a
ambiguity however; there are no mathematical and formal
unified way; 3) lack of a user-friendly tooling support which
representations of this semantics that can be used
discourages the use of the current approaches and limits their
straightforwardly as input to model-checking tools.
adoption by the industry.
To face this issue, we decided to provide a formalization
In the following section we draw the main lines of our
of UML AD semantics based on the fUML specification
approach for process verification called ProVer. Three
instead of relying on a translation of UML AD towards
important design decisions will be highlighted and motivated:
other formalisms such as Petri nets for instance. We aimed
1) the use of UML AD as a process modeling language, 2) the
to define a formal model of fUML using First-Order Logic
formalization of the UML AD concepts for process
(FOL). The formalization addresses a subset of fUML that
verification as well as a well-identified set of properties in
includes the set of concepts required for process modeling as
first-order logic (FOL) and 3) the use of SMT (Satisfiability
identified in [Bendraou 05]. Current formalizations proposed
Modulo Theories) as a mean to verify properties spanning
in the literature focus mainly on the control-flow aspects of
different process’s perspectives in a very optimal way.
the process preventing to verify many kinds of properties
Section 3 gives more details about the role of SMT in ProVer
related to data-flow, resources and timing constraints [Van der
while Section 4 will detail the tooling support and the
Aalst 11]. Therefore, our formalization covers both control
validation aspects. Section 5 concludes this work and draws
and data-flow of the process through the use of the UML AD
future steps of this contribution
notations and takes into account organizational data such as
ProVer: a framework for Process resources and time constraints.
Verification At this aim, we have formally reduced the representation
of a software process to a vertex-labeled graph. Each graph's
The traditional approach to achieve the verification of a node corresponds to a UML Activity node according to its
model (a process model in our case) with respect to a given type (i.e. Control, Executable or Object Node). Each graph's
property consists beforehand in defining the two entities arc corresponds to a UML Activity edge (i.e. Control or
formally: a) the process modeling language concepts and b) Object Flow). The execution semantics of this formalism is
the properties to be verified. A process model is then based on the notions of states, enabling and firing of
submitted to a so-called model-checker tool, which will transitions, similar to those used in the Colored Petri Nets
answer the question of (un)satisfaction of the given property [Jensen 87]. To be able to reason about each dimension of the
by the process model. process, the formalization covers both control and data-flow
In the following sub-sections, we will detail our design of the process through the use of the AD notations, and takes
choices and contributions regarding the ProVer framework. into account the associated organizational data such as
resources and timing constraints. We partially published this
UML Activity Diagram formalization for process modeling: formalization in [Laurent 14] and we extended it for the
our choice of UML as PML was mainly driven by the purpose of this work in order to cover more UML Concepts.
following arguments: Due to space constraints we can introduce it here but the
- UML is a standard and widespread modeling language in interested reader can find it in [Laurent 18].
the industry with a mature tooling support. Once we had formalized the UML AD in FOL, we opted
- UML AD has proven to be a good candidate as PML in for an implementation based on Satisfiability Modulo
many works presented in the literature [Bendraou 10]. Theories (SMT) technologies. SMT is an area of automated
deduction that studies methods for checking the satisfiability
- UML AD has proven to be one of the most expressive of first-order formulas with respect to some logical theory T
languages in terms of satisfying the so well-known of interest [Barret 09]. What distinguishes SMT from general
workflow patterns as presented by [Van Der Aalst 03]. automated deduction is that the background theory T need not
However, the approach presented here can be applied to any be finitely or even first-order axiomatizable, and that
PML such as BPMN but a formalization of BPMN concepts is specialized inference methods are used for each theory. By
required in order to achieve that. This represents the cost to being theory-specific and restricting their language to certain
adapt our approach to other PMLs. classes of formulas (such as, typically but not exclusively,
quantifier-free formulas), these specialized methods can be
One of the main challenges we had to face was that the implemented in solvers that are more efficient in practice than
general-purpose theorem provers. Typical theories of interest possible process's executions. They are related to the Time
include formalizations of various forms of arithmetic, arrays, and Resource perspectives of a process. Examples of such
finite sets, bit vectors, algebraic datatypes, strings, floating properties are to make sure, for instance, that the process or an
point numbers, equality with uninterpreted functions, and activity will terminate before a given deadline whatever the
various combinations of these. These theories are supported execution path, make sure that there will be enough agents to
by a standard called SMT-LIB perform the activities of the process, etc. A detailed
[http://smtlib.cs.uiowa.edu/language.shtml] and are identification and formalization of such properties are then
implemented in many efficient solvers (z3, Yices, CVC4, etc.) required in order to verify them on process models and to
Category Definition
(1) Syntactical
SynWorkflow Syntactical errors on the process (e.g. the source and target of an edge are different)
Syntactical errors on the organizational part of the process (e.g. the same agent cannot be
SynOrganizational
assigned more than one time to the same activity)
(2) Soundness
OptionToComplete A started process can always complete
ProperCompletion No other activity should be running when the process terminates
NoDeadTransition All the activities must be reachable
Soundness with data
MissingData Data is always present when needed (e.g. no data missing to start an activity)
UselessData Data created is always used (e.g. no data created but never used before the process ends)
Data can never be in an inconsistent state (e.g. no data modified by multiple activities in
InconsistentData
parallel)
(3) Organizational
There is enough time to perform the activities (e.g. the process will terminate before X
InTime
hours/days)
MissingResource No missing resource to start an activity (e.g. there are enough agents to do the process)
InefficientResourceUse No resources that are inefficiently used (e.g. the agents have always activity to do)
(4) Business
ExistenceActivity A is executed more / less / (between) X (and Y) times
ExistenceTimeActivity A is executed before / after / (between) X (and Y) time unit
ExistenceTimeData ArtefactA is available before / after/(between) X (and Y) time unit
ExistenceTimeResource ResourceA is used before / after/(between) X (and Y) time unit
Relation A is executed before / after / in-parallel / in-exclusion / (between) B (and C)
RelationData ArtefactA is available before /after / in-exclusion of ArtefactB
ArtefactA is available before / after/in-parallel / in-exclusion / (between) the execution of B
RelationActivityData
(and C)
LogicBased e.g. Existence(A) implies Existence(B) else Existence(C)
…. e.g. Existence(A) implies (ExistenceData(ArtefactA) and ExistenceData(ArtefactB))
Table 1. Overview of the software properties we identified
Categorization of process perspectives and properties: as integrate them into our process verification tool.
mentioned earlier, the literature addresses essentially what it
Once we formalized the UML AD, we also formalized a
is called soundness properties [Van der Aalst 11] which aim
set of process properties that we identified through a detailed
to detect some Behavioral issues on process executions vs.
study of the literature. This set addresses the four process
Syntactical errors. Business processes and more particularly
aspects introduced earlier (Control and Data flow, Time and
software processes are concerned with additional and critical
Resources) plus another one that we called Business
constraints related to their human-oriented nature. They imply
properties which refers to every project’s specific constraints
many creative tasks that rely on many factors such as time,
that have to be defined by the process modelers depending on
human agents and resource management. The success of a
the project’s context. This set comes in the form of a library
software process depends also on the application of many best
of properties described both in natural language and LTL
practices and organizational constraints. We call these
which is the logic we have chosen to express our properties
constraints Organizational properties and we consider them as
and which covered all of them in terms of expressivity. In a
a subcategory of Behavioral properties since a state space
separate work [Khelladi 15], we also studied the four most
exploration is required to guarantee their preservation for all
used software development methods namely RUP, SCRUM, the result into the process model editor.
XP and KANBAN in order to extract from each of them, a set
In the following sections we will zoom-in SMT choice
of best practices and constraints that should be enforced
and the translation details. We will give examples of some
during the development process. This resulted in a ready-to-
concepts and properties expressed in SMT before to present
use library of constraints that we integrated to our process
the graphical interface of our tool. A user guide of the tool
modelling and verification tool so process modelers can
presenting all the details of the GUI is given here
annotate their process models with one of these
[Bendraou16].
Use of SMT for process verification
The verification process that we adopted is the well-
known Bounded Model Checking (BMC) procedure
[Clarke01]. Classically, this procedure inputs, 1) an initial
state (for the system), 2) the transition relation, 3) a property
to verify and, 4) a length bound k, then outputs the
(un)satisfaction of the of system w.r.t the property up the
bound k.
The implementation of such a procedure is done by
Figure 2. ProVer: overview of the approach
constructing a logical formula that is satisfiable if and only if
properties/constraints to make sure that the process model the underling transition system can realize a sequence of k
doesn’t violate any of them. state transitions that satisfy the property. If such a path
Table 1 depicts the set of properties we identified and segment cannot be found at the given length k, the search
their categorization. continues for larger k. The procedure is symbolic, i.e.,
symbolic Boolean variables are utilized; thus, when a check is
Now that we have introduced the formalization of both the done for a specific path segment of length k, all path segments
PML and the properties, the next sub-section gives an of length k are being examined. The formula that is formed is
overview of the ProVer tool. given to a satisfiability solving program and if a satisfying
Overview of the approach. In this section, we briefly assignment is found, that assignment is a witness for the path
highlight the different steps required to run a process model segment of interest.
verification using ProVer, then we present its internal
architecture and the steps we followed in order to build this
framework.
First, the process modeler needs either to design a process
model or to import an existing one (see (1) in figure 2). In our
tool, UML AD is used as a process modeling language.
Secondly, the process modelers can choose among the library
of predefined properties proposed by ProVer and which Figure 3. A process model with UML AD representing a
covers different process perspectives (Control/ Data flow, selling process
Time or Resources). This is done either by checking boxes If the formula is propositional and not very large then a basic
(see (2.a) in figure 2) or by using an annotation-based Boolean SAT-solver can solve it efficiently. Things become
language we defined in [Khelladi 15] (see (2.b) in figure 2). more complicated when the formula is FOL! Actually, a first
Process models and the properties are then translated into attempt to solve such formula is to transform it to
SMT specification which implements the semantics of UML propositional one and use SAT-solvers. However, this
AD as defined by our FOL formalization and based on the transformation is memory and time consuming and, most of
fUML standard (see (3) in figure 2). The SMT solver all degenerative! For example, when comparing two 32-bits
performs the verification (see (4) in figure 2) and if a counter- integer variables, we have to use 64 binary variables and
example is found, this is highlighted in the process model compare them bitwise. So, the approach will have serious
editor on the process model in red with a message of the efficiency issues when the treated models are large.
unsatisfied property (see (5) in figure 2).
The other option is to explore Satisfiability Modulo Theories
As we can see in the figure, the steps we followed in order to (SMT). This area handles FOL formulae directly by use of
realize ProVer were 1) formalization of UML AD semantics simple transformation based on the SMT-LIB standard
as well as the set of properties in FOL; 2) implementation of
[Barret 15]. The SMT option seems to be very promising and
the UML AD / Properties semantics and UML AD syntax in
is strengthened by the results obtained by SMT-solvers in the
SMT; 3) implementation of the translations from UML AD/
last SMT competitions (2014 and 2015).
Properties specifications => SMT; 3) graphical integration of
Property Alloy4SPV ProVer Speed Up Result
Check Completion 24 0.8 30 Verified
Run Completion 33 1.5 22 Model Found
Check Total Time 6 154 2 64 Verified
Run Total Time 6 63 2 23 Model Found
Check Existence Reserve Counter Example
20 2 10
Stock = 0 Found
Run Existence Reserve
22 1 22 Model Found
Stock = 0
Table 2. Alloy approach (Alloy4SPV, with Alloy Analyzer) Vs. SMT-based approach (ProVer with z3 solver),
performance for properties expressed on the process on figure 3.
ProcessModel
er
Front-end
< <
> UML
fUML> AD Verification Obeo
plugin Tool
VerificationQuery:ProcessPrope ProcessModel:UMLA
rty
<
>
FOL2SMT Translator
Back-end
VerificationQuery:SMTProble ProcessModel:SMTProblem
m
<
> SMT-
Solver
VerificationResult : SMTSolution
Figure 4. Architecture of the ProVer tool
Actually, solvers, like z3 (form Microsoft), Yices (from some properties verification on another example, the OpenUP
SRI International), show their ability to solve very process, not presented here. The next section gives more
complicated problems (from both academic and industrial details about ProVer architecture.
worlds) in a reasonable time.
Tooling support: architecture and
To give an idea on the effectiveness of our SMT-based
approach, we use an example representing a selling process validation.
(see Figure. 3). The process includes 7 activities and 4 The architecture of our tool is highlighted in Fig. 4. It is based
decision nodes (one from each type). Table 2 shows some on the two classical layers: the front-end and the back-end.
results comparing our SAT-based approach (implemented in The former allows the interaction with the final user in a
Alloy4SPV [Laurent 14b]) with respect to the SMT-based friendly graphical way. It inputs the UML AD representing
one. The first column of Table 2 represents the checked the business process as well as the properties to be analysed.
properties, while the second highlights the execution time (in It outputs the result of the verification. The Obeo UML Tool
seconds) with Alloy4SPV. The third column mentions the component is dedicated to the input of the studied process
execution time of our ProVer tool (SMT-based) and the last model and the output of the verification result, while the
column exhibits the result of the verification. We can clearly FUML AD Verification plugin component deals with the input
notice here the efficiency of our SMT-based approach just by of the properties to be verified. It is worth noting that no
looking the speed up we obtain for each property. mathematical background is needed to operate these inputs
The results obtained so far are very interesting i.e. 64x and interpret the results. All the properties can be selected
faster in the example shown above and up to 92x faster for through an integrated and ready to use library of properties.
Due to space limit we can’t present in details the GUI of the - fireStart(Dec,t) = (and (= (select XToDec (+ t 1))
(- (select XToDec t) 1))
tool but a user guide can be found here [Bendraou 16]. A ; Remove a token from XToDec
java-like annotation language has also been developed to ease (= (select Dec (+ t 1)) (+ (select Dec t) 1))
; Add a token to Dec
the specification of customized properties [Khelladi 15]. (= (select DecToY (+ t 1)) (= (select DecToY t) 1))
The two other components are FOL2SMT Translator and the ; Between t and t+1 instants the marking
of DecToY must remain the same
SMT-solver components form the back-end. The former is the (= (select DecToZ (+ t 1)) (= (select DecToZ t) 1))
heart of the tool. It implements the verification request of the ; Between t and t+1 instants the marking
user as a FOL formula that is written in the SMT-LIB of DecToZ must remain the same )
language. The produced SMT problem is then submitted to - fireFinish(Dec,t) = (and (= (select Dec (+ t 1))
the SMT-solver component that resolves it. The result of that (- (select Dec t) 1))
; Remove a token from XToDec
resolution is a feedback that is directly highlighted in the (= (select XtoDec (+ t 1)) (select XToDec t))
process model editor tool in a user friendly way. If the ; Between t and t+1 instants the marking
of XToDec must remain the same
property is violated then an example (a path) of such a (or (and (= (select DecToY (+ t 1))
violation is highlighted. (+ (select DecToY t) 1))
Since the most complicated part in our tool is the one (= (select DecToZ (+ t 1))
(select DecToZ t)))
dedicated to the translation of a FOL formula to the SMT-LIB ; Move the token to DecToY (choice 1)
language, let us give some hints about its implementation by (and (= (select DecToY (+ t 1))
(select DecToY t))
mean of a very simple example. (= (select DecToZ (+ t 1))
(+ (select DecToZ t) 1)))
Consider the Figure 5. A decision node in an AD ; Move the token to DecToZ (choice 2)
AD element of ))
figure 5. It is a Actually, we operate such a transformation for all
decision node elements of AD that are necessary for the modeling of
(called Dec), that business processes. The implementation of this transformation
inputs the XtoDec needed nearly 2000 lines of code in java.
arc and outputs two
arcs: DecToY and
Conclusion
DecToZ. According The most important contributions of this work are (i) the
to the semantics identification of a reusable and configurable library of
defined in [Laurent 14], the execution of such a node properties addressing all the process aspects (control, data
considers two situations: (i) the node is ready to start; (ii) the flow, time and resources), (ii) the formalization of this
node is ready to finish. The former case is identified by the library as well as the UML AD semantics in first order
presence of a token on the input arc and the absence of any on logic. This makes these definitions reusable for any other
the decision node. In this case, the resulting action consists in purposes such as the mapping to other model-checker
moving the token from the input arc to the node. The later formalism. In our case we opted for SMT theories.
case is formalized by the presence of token on the decision
node. Here, the resulting action is to move the token from the The second undeniable contribution is the integration
node to one of the outputs (chosen arbitrarily). and the verification of all process perspectives in a unified
and integrated way thanks to our formalization and of our
If we note by enableStart(Dec, t) the predicate that use of SMT theories, within a user-friendly tool for process
represents the case (i) at time stamp t and enableFinish(Dec,t) verification and execution. This framework has been adopted
the predicate that represents the case (ii) at time stamp t, then by our MeRGE industrial partners (European project)
using the SMT-LIB language we can write: [MeRGE 12] and integrated to the MeRGE platform, an EMF
- enableStart(Dec,t)=(and (>(select XToDec t) eclipse framework for the development of safety critical
0) (=(select Dec t)0) systems.
- enableFinish(Dec,t) = (>(select Dec t)0)
Regarding our feedback using SMT for process
Actually, Dec, XtoDec, DecToY and DecToZ are verification it can be summarized in the following points: (1)
represented as arrays of integers indexed by integers. Each handling complex constraints in a compact way, hence saving
entry of these arrays defines the “marking” (number of memory; (2) treating specific constraints with dedicated
tokens) of the element at the given time stamp. For example, algorithms, hence saving time.
(select Dec t) returns the marking of Dec at time t.
We are currently working on the validation of our
Similarly, if we consider fireStart(Dec,t) as the predicate approach on bigger process models from the Healthcare
that starts the execution of the decision node at time stamp t, domain (more than 200 activities). We are also investigating
while fireFinish(Dec,t) the one that terminates its execution, the difference in performance according the property checked
we obtain the following encoding: and the solver used. Indeed, in our experiments, the
verification time for some properties was different from one
solver into another.
[Mendling 06] J an Mendling et al.. Faulty epcs in the sap reference
References model. In Buss. Proc. Manag., pp 451–457. Springer, 2006.
[Awad 07] Awad. Bpmn-q : A language to query business processes. [Laurent 14] Y. Laurent et al. “Formalization of fUML: An Application to
In EMISA, volume 119, pages 115–128, 2007 Process Verification”, CAiSE 2014, Springer, pp . 347-363
[Awad 09] A. Awad et al. “Specification, verification and explanation of [Laurent 14b] Y. Laurent et al. Alloy4SPV : a Formal Framework for
violation for data aware compliance rules”. In Service-Oriented Software Process Verification, 10th ECMFA, LNCS, pp.83-100, 2014
Computing, pp 500–515. Springer, 2009 [Laurent 18] Y. Laurent’s PhD Thesis document, LIP6, March 2018,
[Barret 09] C. Barrett et al. Satisfiability Modulo Theories. In A. Biere, https://drive.google.com/open?id=14p9i4ulLacjdUIgFhZKUVI0wfQa4x6hP
Marij J. H. Heule, H. van Maaren, and T. Walsh, editors, Handbook of [Liu 07]Liu, Y., et. al.: A static compliance-checking framework for
Satisfiability, Vo. 185, chapter 26, pp 825–885. IOS Press, Feb. 2009. business process models. IBM Systems Journal 46(2) (2007) 335-361
[Barret 15] C. Barrett et al. The SMT-LIB Standard: Version 2.5. In [Mendling 07] Jan Mendling, Gustaf Neumann, and Wil Van Der Aalst.
Tec. report of Dep. of Comp. Science, The University of Iowa. 2015. Understanding the occurrence of errors in process models based on
[Bendraou 05] R. Bendraou et al. "UML4SPM : A UML2.0-Based metrics. In On the Move to Meaningful Internet Systems 2007 :
metamodel for Software Process Modeling", in Proceedings of the CoopIS, DOA, ODBASE, GADA, and IS, pp 113–130. Springer, 2007.
ACM/IEEE 8th International Conference on Model Driven Engineering [Mendling 09] Jan Mendling. Empirical studies in process model
Languages and Systems (MoDELS’05), Montego Bay, Jamaica, Oct. verification. In TPNOMC II, pp 208–224. Springer, 2009.
2005, LNCS, Vol. 3713, PP 17-38
[MeRGE 12] Merge, ITEA project, safety & security. http://www.merge-
[Bendraou 10] R. Bendraou et al. “A comparison of six uml-based project.eu/. last vist Oct 2015.
languages for software process modeling”.Trans. Software Eng. 2010
[Morimoto 08] S.Morimoto. A survey of formal verification for business
[Bendraou 16] ProVer Guide: process modeling. In Computational Science–ICCS 2008, pages 514–
https://pagesperso.lip6.fr/Reda.Bendraou/sites/Reda.Bendraou/IMG/p 522. Springer, 2008
df/prover_user_guide.pdf
[OMG 11] Object Management Group (OMG). Business process
[Christov 14] S.C. Christov, G. S. Avrunin , L.A. Clarke, American model and notation (bpmn) version 2.0, jan 2011
Medical Informatics Association Annual Symposium (AMIA 2014),
[OMG 11b] OMG. Semantics of a foundational subset for executable
November 15-17, 2014, Wash., DC, pp. 395-404. (UM-CS-2014-022)
uml models (fuml) version 1.0. http: //www.omg.org/spec/FUML/, 2011
[Clarke01] E. Clarke et al. Model Checking Using Satisfiability Solving.
[Peterson 81] Peterson J.L. Petri net theory and the modeling of
In journal of FMSD. Kluwer Academic Publishers. July 2001.
systems. 1981. 5, 29
[Dijkman 08] R.M. Dijkman et al. “Semantics and analysis of business
[Pnueli 77] A. Pnueli. The temporal logic of programs. In FCS, pp 46–
process models in bpmn”. Information and Software Technology,
57. 1977.
50(12) :1281–1294, 2008
[Simidchieva 10] B I. Simidchieva, et al., Proceedings of the 2010
[Eshuis 02] Eshuis H. “Semantics and verification of uml activity
Electronic Voting Technology Workshop/Workshop on Trustworthy
diagrams for workflow modelling”. 2002
Elections (EVT/WOTE '10), August 9-10, 2010, Washington, DC.
[Emerson 90] E.A. Emerson. Temporal and modal logic. “Handbook of
[Smith 02] R.L Smith et al. An approach supporting property
Theoretical Computer Science” Volume B. Formal Models and
elucidation. In Proceedings of the 24th ICSE., pp 11–21. ACM, 2002
Semantics (B), 995 :1072, 1990
[Trcka 09] N. Trcka et al. Data-flow anti-patterns: Discovering data-
[Eshuis 06] H. Eshuis. “Symbolic model checking of uml activity
flow errors in workflows. In CAISE, Springer (2009). 425-439.
diagrams”. TOSEM 15(1), (2006) 1-38
[Van der Aalst 98] van der Aalst, W.M.: The application of petri nets to
[Fahland 09] D. Fahland et al. “Instantaneous soundness checking of
workflow management. JCSC 8(01) (1998) 21-66.
industrial business process models”. BPM. 2009. 278-293
[Van der Aalst 99] van der Aalst, W.M. Formalization and verification
[Hafer 87] Hafer and Wolfgang Thomas. “Computation tree logic ctl*
of event-driven process chains. IST, 41(10): 639–650, 1999
and path quantifiers in the monadic theory of the binary tree”. In
Automata, Lang. and Prog., pp 269–279. Springer 1987 [Van Der Aalst 03] van Der Aalst, W.M., Ter Hofstede, A.H.,
Kiepuszewski, B., Barros, A.P.: Workflow patterns. Distributed and
[Hofstede 02] T.Hofstede, A.: Workflow patterns: On the expressive
parallel databases 14(1) (2003) 5, 51
power of petri-net-based workflow languages. In: of DAIMI, University
of Aarhus, Citeseer (2002) [Van der Aalst 11] van der Aalst,et al. “Soundness of workflow nets:
classification, decidability, and analysis”. Formal Aspects of
[Guelfi 05]Guelfi, N., Mammar, A.: A formal semantics of timed activity
Computing 23(3) (2011) 333-363
diagrams and its promela translation. In: Software Engineering
Conference, 2005. APSEC'05. 12th Asia-Pacific, IEEE (2005) [Vanhatalo 07] J.Vanhatalo et al.. Faster and more focused control-
flow analysis for business process models through sese
[Gruhn 06] V. Gruhn and R.Laue. “Complexity metrics for business
decomposition. In ICSOC 2007, pp 43–55. Springer, 2007. 3, 33, 143
process models”. In 9th international conference on business
information systems (BIS 2006), volume 85, pages 1–12, 2006. [Watahiki 11]K. Watahiki et al. Formal verification of business
processes with temporal and resource constraints. In Systems, Man,
[Gruhn 07] V.Gruhn and R. Laue.” What business process modelers
and Cybernetifcs (SMC), pp1173–1180., 2011
can learn from programmers”. S. of Comp. Prog., 65(1) :4–13, 2007.
[Wohed 05] Wohed et al. Pattern-based analysis of the control-ow
[Khelladi 15]D. Khelladi et al. A framework to formally verify
perspective of uml activity diagrams. In: Conceptual Modeling ER
conformance of a software process to a software method. SAC 2015 :
2005. Springer (2005) 63-78
1518-1525
[Wong 07] Wong, P., Gibbons, J.: A process-algebraic approach to
[Knuplesch 10] D. Knuplesch et al. On enabling data-aware
workflow specification and refinement. In: Software Composition,
compliance checking of business process models. Con. Modeling–ER
Springer (2007) 51-65
2010, pages 332–346, 2010
[Kleppe 03] A. Kleppe et al. The model driven architecture:
practice and promise, 2003
[Jensen 87] K. Jensen. Coloured petri nets. Springer, 1987
[Jung 10] Jung, H.T., Joo, S.H.: Transformation of an activity model
colored petri net model. In: TISC, IEEE (2010) 32-37