Information Technology Reference
In-Depth Information
algorithm is used to determine which nodes do not satisfy their eventualities. These
nodes are removed and the reachability algorithm is reapplied until no nodes may be
removed. The set of formulae
Γ
is satisfiable, if and only if the root node has not been
removed [24]. Further, the graph created by the tableau algorithm, referred to as the
pseudomodel
, describes all possible formula-models, i.e., possible traces [24]. We use
this pseudomodel to extract possible traces during our synthesis approach.
3
Synthesis of Process Templates from Compliance Rules
In this section, we describe our approach to the synthesis of process models from a set
of compliance rules expressed in temporal logic. First, Section 3.1 gives an overview
of the approach and introduces an example set of compliance rules used to illustrate all
subsequent steps. Section 3.2 describes the LTL encoding of the compliance rules and
additional domain knowledge. Section 3.3 elaborates on the extraction of traces from a
behavioral model, while Section 3.4 focuses on consistency of these traces. Synthesis
of a process template from these traces is discussed in Section 3.5. Finally, we elaborate
on the evaluation of synthesized templates in Section 3.6.
3.1
Overview
The process model in Fig. 1 visualizes the steps to synthesize a process template out
of a set of compliance rules. First, a set of compliance rules is collected. In order to
identify whether these requirements are consistent and thus a process template can be
synthesized, related domain-specific knowledge is identified. In Section 3.2 we give
details on the LTL encoding of both compliance rules and domain knowledge.
For the conjunction of these LTL formulae, we verify satisfiability as it has been
summarized in Section 2.3. If the set is not satisfiable then no trace can be constructed
to satisfy the given LTL formulae so the inconsistency is reported to the user. If the
set is satisfiable then the satisfiability checker automatically returns the pseudomodel
which is a behavioral model of all traces that obey the given constraints.
As a next step, finite traces are extracted from the pseudomodel by following all
choice points and stopping when a trace becomes cyclic. We focus on this step in Sec-
tion 3.3. Having a finite set of traces that satisfy the compliance rules, we check it for
Rules are
inconsistent
Add extra
domain
knowledge in
LTL
No
Check LTL
satisfiability;
generate
pseudomodel
Collect related
compliance
rules in LTL
Is there a
pseudomodel?
Analyze
generated
model
Is it possible to
generate a
process model?
Yes
Yes
Are there any
descrepencies?
Generate
process model
No
Extract traces
Analyze traces
Refine
compliance
rules or domain
knowledge
No
Yes
Fig. 1.
Process Synthesis Approach
