Login / Sign Up
BPMN Business Management Presentations Process Analysis Process Management Process Modeling
Contributed on September 12, 2014
Loading 7.1K
2K

Where did I go wrong? Explaining errors in process models

Description

This presentation shows how to reduce diagnostic information returned by general purpose model checkers (counter example paths) to essential parts that help understanding the error. The presentation has been given at the 12th International Conference on Business Process Management (BPM’14), September 2014 in Eindhoven.

Transcript

Where did I go wrong?
Explaining errors in process models
Niels Lohmann @nlohmann
Dirk Fahland @dfahland Verification of processes and services
2
process model
property
verification technique
diagnostic information Verification of processes and services
3
verification technique
diagnostic information
BPMN
Soundness
domain-specific
high-quality Verification of processes and services
4
CMMN
Declare
WS-BPEL
WS-Policy
EPC
BPMN
YAWL
Object Life-Cycles
GSM
Rules
Soundness
Security
Compliance
Conformance to …
diagnostic information
verification technique
domain-specific
high-quality
-moving target
-domain-specific approaches too specific to follow Verification of processes and services
5
CMMN
Declare
WS-BPEL
WS-Policy
EPC
BPMN
YAWL
Object Life-Cycles
GSM
Rules
Soundness
Security
Compliance
Conformance to …
diagnostic information
verification technique
high-quality
general purpose Model checking
general purpose verification approach:
1. formalize model and specification*
2. push a button
6
*can be hidden from the user Effectiveness and efficiency
-model checking works in reality
-successful applications in many domains
-very fast: “verify while you model”
7 Diagnosis
-in case of error: outputs target state and produce a witness path
-describes how target state can be reached
-operational semantics: can be simulated
8
witness path
target state Diagnosis: the bad
PATH process.s00000823##s00006200.inputCriterion.s00001053 fork.s00001071.activate.s00001072 fork.s00001071.fire.s00001078 merge.s00001061.activate.s00001065 merge.s00001061.fire.s00001069 callToTask.s00006202.inputCriterion.s00001053 callToTask.s00006202.outputCriterion.s00001055 callToTask.s00006211.inputCriterion.s00001053 callToTask.s00006211.outputCriterion.s00001055 callToTask.s00006209.inputCriterion.s00001053 callToTask.s00006209.outputCriterion.s00001055 decision.s00001158.activate.s00001072 decision.s00001158.fire.s00001075 merge.s00001160.activate.s00001064 merge.s00001160.fire.s00001069 callToTask.s00006203.inputCriterion.s00001053 callToTask.s00006203.outputCriterion.s00001055 callToTask.s00006214.inputCriterion.s00001053 callToTask.s00006214.outputCriterion.s00001055 callToTask.s00006213.inputCriterion.s00001053 callToTask.s00006213.outputCriterion.s00001055 decision.s00001840.activate.s00001072 decision.s00001840.fire.s00001075 callToTask.s00006201.inputCriterion.s00001053 callToTask.s00006201.outputCriterion.s00001055 decision.s00001123.activate.s00001072 decision.s00001123.fire.s00001075 merge.s00001161.activate.s00001064 merge.s00001161.fire.s00001069 callToTask.s00006208.inputCriterion.s00001053 callToTask.s00006208.outputCriterion.s00001055
decision.s00001157.activate.s00001072
decision.s00001157.fire.s00001073
fork.s00001071.fire.s00001073
merge.s00001061.activate.s00001064
join.s00001163.activate.s00001062
merge.s00001061.fire.s00001069
join.s00001163.activate.s00001064
merge.s00001162.activate.s00001062
merge.s00001162.fire.s00001069
callToTask.s00006210.inputCriterion.s00001053
callToTask.s00006210.outputCriterion.s00001055
decision.s00001159.activate.s00001072
decision.s00001159.fire.s00001073
join.s00001163.activate.s00001065
join.s00001163.fire.s00001069
fork.s00001071.fire.s00001075
merge.s00001160.activate.s00001065
callToTask.s00006207.inputCriterion.s00001053
merge.s00001160.fire.s00001069
callToTask.s00006207.outputCriterion.s00001055
callToTask.s00006203.inputCriterion.s00001053
decision.s00001126.activate.s00001072
callToTask.s00006203.outputCriterion.s00001055
decision.s00001126.fire.s00001073
callToTask.s00006214.inputCriterion.s00001053
callToTask.s00006202.inputCriterion.s00001053
callToTask.s00006202.outputCriterion.s00001055
callToTask.s00006211.inputCriterion.s00001053
callToTask.s00006211.outputCriterion.s00001055
callToTask.s00006209.inputCriterion.s00001053
callToTask.s00006209.outputCriterion.s00001055
decision.s00001158.activate.s00001072
decision.s00001158.fire.s00001075
callToTask.s00006214.outputCriterion.s00001055
callToTask.s00006213.inputCriterion.s00001053
callToTask.s00006213.outputCriterion.s00001055
decision.s00001840.activate.s00001072
decision.s00001840.fire.s00001075
callToTask.s00006201.inputCriterion.s00001053
callToTask.s00006201.outputCriterion.s00001055
decision.s00001123.activate.s00001072
decision.s00001123.fire.s00001073
callToTask.s00006204.inputCriterion.s00001053
callToTask.s00006204.outputCriterion.s00001055
callToTask.s00003714.inputCriterion.s00001053
callToTask.s00003714.outputCriterion.s00001055
callToTask.s00006215.inputCriterion.s00001053
callToTask.s00006215.outputCriterion.s00001055
callToTask.s00006206.inputCriterion.s00001053
join.s00001163.activate.s00001064
callToTask.s00006206.outputCriterion.s00001055
callToTask.s00006205.inputCriterion.s00001053
callToTask.s00006205.outputCriterion.s00001055
merge.s00001161.activate.s00001062
merge.s00001161.fire.s00001069
callToTask.s00006208.inputCriterion.s00001053
callToTask.s00006208.outputCriterion.s00001055
decision.s00001157.activate.s00001072
decision.s00001157.fire.s00001073
join.s00001163.activate.s00001062
callToTask.s00006212.inputCriterion.s00001053
callToTask.s00006212.outputCriterion.s00001055
merge.s00001162.activate.s00001064 merge.s00001162.fire.s00001069 callToTask.s00006210.inputCriterion.s00001053 callToTask.s00006210.outputCriterion.s00001055 decision.s00001159.activate.s00001072 decision.s00001159.fire.s00001073 join.s00001163.activate.s00001065 join.s00001163.fire.s00001069 callToTask.s00006207.inputCriterion.s00001053 callToTask.s00006207.outputCriterion.s00001055 decision.s00001126.activate.s00001072 decision.s00001126.fire.s00001073 STATE decision.s00001126.output.s00001054 : 2
-paths can become very long
-length correlates with size of the model
-reports all events equally: disregarding importance This talk: better diagnosis
PATH process.s00000823##s00006200.inputCriterion.s00001053 fork.s00001071.activate.s00001072 fork.s00001071.fire.s00001078 merge.s00001061.activate.s00001065 merge.s00001061.fire.s00001069 callToTask.s00006202.inputCriterion.s00001053 callToTask.s00006202.outputCriterion.s00001055 callToTask.s00006211.inputCriterion.s00001053 callToTask.s00006211.outputCriterion.s00001055 callToTask.s00006209.inputCriterion.s00001053 callToTask.s00006209.outputCriterion.s00001055 decision.s00001158.activate.s00001072 decision.s00001158.fire.s00001075 merge.s00001160.activate.s00001064 merge.s00001160.fire.s00001069 callToTask.s00006203.inputCriterion.s00001053 callToTask.s00006203.outputCriterion.s00001055 callToTask.s00006214.inputCriterion.s00001053 callToTask.s00006214.outputCriterion.s00001055 callToTask.s00006213.inputCriterion.s00001053 callToTask.s00006213.outputCriterion.s00001055 decision.s00001840.activate.s00001072 decision.s00001840.fire.s00001075 callToTask.s00006201.inputCriterion.s00001053 callToTask.s00006201.outputCriterion.s00001055 decision.s00001123.activate.s00001072 decision.s00001123.fire.s00001075 merge.s00001161.activate.s00001064 merge.s00001161.fire.s00001069 callToTask.s00006208.inputCriterion.s00001053 callToTask.s00006208.outputCriterion.s00001055
decision.s00001157.activate.s00001072
decision.s00001157.fire.s00001073
fork.s00001071.fire.s00001073
merge.s00001061.activate.s00001064
join.s00001163.activate.s00001062
merge.s00001061.fire.s00001069
join.s00001163.activate.s00001064
merge.s00001162.activate.s00001062
merge.s00001162.fire.s00001069
callToTask.s00006210.inputCriterion.s00001053
callToTask.s00006210.outputCriterion.s00001055
decision.s00001159.activate.s00001072
decision.s00001159.fire.s00001073
join.s00001163.activate.s00001065
join.s00001163.fire.s00001069
fork.s00001071.fire.s00001075
merge.s00001160.activate.s00001065
callToTask.s00006207.inputCriterion.s00001053
merge.s00001160.fire.s00001069
callToTask.s00006207.outputCriterion.s00001055
callToTask.s00006203.inputCriterion.s00001053
decision.s00001126.activate.s00001072
callToTask.s00006203.outputCriterion.s00001055
decision.s00001126.fire.s00001073
callToTask.s00006214.inputCriterion.s00001053
callToTask.s00006202.inputCriterion.s00001053
callToTask.s00006202.outputCriterion.s00001055
callToTask.s00006211.inputCriterion.s00001053
callToTask.s00006211.outputCriterion.s00001055
callToTask.s00006209.inputCriterion.s00001053
callToTask.s00006209.outputCriterion.s00001055
decision.s00001158.activate.s00001072 decision.s00001158.fire.s00001075 callToTask.s00006214.outputCriterion.s00001055 callToTask.s00006213.inputCriterion.s00001053 callToTask.s00006213.outputCriterion.s00001055 decision.s00001840.activate.s00001072 decision.s00001840.fire.s00001075 callToTask.s00006201.inputCriterion.s00001053 callToTask.s00006201.outputCriterion.s00001055 decision.s00001123.activate.s00001072 decision.s00001123.fire.s00001073 callToTask.s00006204.inputCriterion.s00001053 callToTask.s00006204.outputCriterion.s00001055 callToTask.s00003714.inputCriterion.s00001053 callToTask.s00003714.outputCriterion.s00001055 callToTask.s00006215.inputCriterion.s00001053 callToTask.s00006215.outputCriterion.s00001055 callToTask.s00006206.inputCriterion.s00001053 join.s00001163.activate.s00001064 callToTask.s00006206.outputCriterion.s00001055 callToTask.s00006205.inputCriterion.s00001053 callToTask.s00006205.outputCriterion.s00001055 merge.s00001161.activate.s00001062 merge.s00001161.fire.s00001069 callToTask.s00006208.inputCriterion.s00001053 callToTask.s00006208.outputCriterion.s00001055 decision.s00001157.activate.s00001072 decision.s00001157.fire.s00001073 join.s00001163.activate.s00001062 callToTask.s00006212.inputCriterion.s00001053 callToTask.s00006212.outputCriterion.s00001055
merge.s00001162.activate.s00001064
merge.s00001162.fire.s00001069
callToTask.s00006210.inputCriterion.s00001053
callToTask.s00006210.outputCriterion.s00001055
decision.s00001159.activate.s00001072
decision.s00001159.fire.s00001073
join.s00001163.activate.s00001065
join.s00001163.fire.s00001069
callToTask.s00006207.inputCriterion.s00001053
callToTask.s00006207.outputCriterion.s00001055
decision.s00001126.activate.s00001072
decision.s00001126.fire.s00001073
STATE decision.s00001126.output.s00001054 : 2
This talk: better diagnosis
path
essential path
distill
Why useless? Reasons for useless paths
12
detours
depth-first search
indisputable parts
bootstrapping
interleavings
concurrency Running example
13
lack of synchronization Reduction: obvious parts
-classify transitions
-only report points of alternative continuations*
14
* XOR-gateways, events, exceptions, …
assume progress of flow Reduction: obvious parts
15
t1
t2
t9
t10
t11
t12
t14
t8
t2
t3
t4
t5
“down”
“down”
“up” Non-obvious “core” of a path ≈ 10-25%
16 Reduction: spurious decisions
-can be found by model checking
-results: 50%-80% spurious, occasionally no reduction (timeout)
17
p1
p3
p2
p4
p5
p6
p1
p3
p5
p6
genuine decision
spurious decision = irrelevant for outcome Reasons for useless paths
18
detours depth-first search
indisputable parts bootstrapping
interleavings
concurrency Reduction: unorder steps
-idea: show independence of steps ( partially ordered runs)
-makes synchronization points (milestones) explicit
19
independent steps
many paths to same goal state order of steps irrelevant Reduction: unorder steps
20
t1
t2
t9
t10
t11
t12
t14
t8
t2
t3
t4
t5
t9
t14
t3 More aid: preserve reference points
21
t1
t2
t9
t10
t11
t12
t14
t8
t2
t3
t4
t5
t9
t14
t3
p1
p6
p6
t5
t11
t10
t1 Final: remove obvious/spurious parts
22
t1
t2
t9
t10
t11
t12
t14
t8
t2
t3
t4
t5
t9
t14
t3
p1
p6
p6
t5
t11
t10
t1 Essential path: find source of error
PATH
process.s00000823##s00006200.inputCriterion.s00001053
fork.s00001071.activate.s00001072
fork.s00001071.fire.s00001078
merge.s00001061.activate.s00001065
merge.s00001061.fire.s00001069
callToTask.s00006202.inputCriterion.s00001053
callToTask.s00006202.outputCriterion.s00001055
callToTask.s00006211.inputCriterion.s00001053
callToTask.s00006211.outputCriterion.s00001055
callToTask.s00006209.inputCriterion.s00001053
callToTask.s00006209.outputCriterion.s00001055
decision.s00001158.activate.s00001072
decision.s00001158.fire.s00001075
merge.s00001160.activate.s00001064
merge.s00001160.fire.s00001069
callToTask.s00006203.inputCriterion.s00001053
callToTask.s00006203.outputCriterion.s00001055
callToTask.s00006214.inputCriterion.s00001053
callToTask.s00006214.outputCriterion.s00001055
callToTask.s00006213.inputCriterion.s00001053
callToTask.s00006213.outputCriterion.s00001055
decision.s00001840.activate.s00001072
decision.s00001840.fire.s00001075
callToTask.s00006201.inputCriterion.s00001053
callToTask.s00006201.outputCriterion.s00001055
decision.s00001123.activate.s00001072
decision.s00001123.fire.s00001075
merge.s00001161.activate.s00001064
merge.s00001161.fire.s00001069
callToTask.s00006208.inputCriterion.s00001053
callToTask.s00006208.outputCriterion.s00001055
decision.s00001157.activate.s00001072
decision.s00001157.fire.s00001073
fork.s00001071.fire.s00001073
merge.s00001061.activate.s00001064
join.s00001163.activate.s00001062
merge.s00001061.fire.s00001069
join.s00001163.activate.s00001064
merge.s00001162.activate.s00001062
merge.s00001162.fire.s00001069
callToTask.s00006210.inputCriterion.s00001053
callToTask.s00006210.outputCriterion.s00001055
decision.s00001159.activate.s00001072
decision.s00001159.fire.s00001073
join.s00001163.activate.s00001065
join.s00001163.fire.s00001069
fork.s00001071.fire.s00001075
merge.s00001160.activate.s00001065
callToTask.s00006207.inputCriterion.s00001053
merge.s00001160.fire.s00001069
callToTask.s00006207.outputCriterion.s00001055
callToTask.s00006203.inputCriterion.s00001053
decision.s00001126.activate.s00001072
callToTask.s00006203.outputCriterion.s00001055
decision.s00001126.fire.s00001073
callToTask.s00006214.inputCriterion.s00001053
callToTask.s00006202.inputCriterion.s00001053
callToTask.s00006202.outputCriterion.s00001055
callToTask.s00006211.inputCriterion.s00001053
callToTask.s00006211.outputCriterion.s00001055
callToTask.s00006209.inputCriterion.s00001053
callToTask.s00006209.outputCriterion.s00001055
decision.s00001158.activate.s00001072
decision.s00001158.fire.s00001075
callToTask.s00006214.outputCriterion.s00001055
callToTask.s00006213.inputCriterion.s00001053
callToTask.s00006213.outputCriterion.s00001055
decision.s00001840.activate.s00001072
decision.s00001840.fire.s00001075
callToTask.s00006201.inputCriterion.s00001053
callToTask.s00006201.outputCriterion.s00001055
decision.s00001123.activate.s00001072
decision.s00001123.fire.s00001073
callToTask.s00006204.inputCriterion.s00001053
callToTask.s00006204.outputCriterion.s00001055
callToTask.s00003714.inputCriterion.s00001053
callToTask.s00003714.outputCriterion.s00001055
callToTask.s00006215.inputCriterion.s00001053
callToTask.s00006215.outputCriterion.s00001055
callToTask.s00006206.inputCriterion.s00001053
join.s00001163.activate.s00001064
callToTask.s00006206.outputCriterion.s00001055
callToTask.s00006205.inputCriterion.s00001053
callToTask.s00006205.outputCriterion.s00001055
merge.s00001161.activate.s00001062
merge.s00001161.fire.s00001069
callToTask.s00006208.inputCriterion.s00001053
callToTask.s00006208.outputCriterion.s00001055
decision.s00001157.activate.s00001072
decision.s00001157.fire.s00001073
join.s00001163.activate.s00001062
callToTask.s00006212.inputCriterion.s00001053
callToTask.s00006212.outputCriterion.s00001055
merge.s00001162.activate.s00001064
merge.s00001162.fire.s00001069
callToTask.s00006210.inputCriterion.s00001053
callToTask.s00006210.outputCriterion.s00001055
decision.s00001159.activate.s00001072
decision.s00001159.fire.s00001073
join.s00001163.activate.s00001065
join.s00001163.fire.s00001069
callToTask.s00006207.inputCriterion.s00001053
callToTask.s00006207.outputCriterion.s00001055
decision.s00001126.activate.s00001072
decision.s00001126.fire.s00001073 Results: typical reduced paths
24
2x lack of synchronization
improper completion
deadlock Summary
-general purpose verification more user friendly
-paths  partial order of important decisions
-applicable to any verification goal
-keep reference points to aid diagnosis Next steps
-error localization vs. explanation
-detect useless cycles
-How should a good diagnosis for $problem look like?
25 Where did I go wrong?
Explaining errors in process models
Niels Lohmann

Leave a Comment

Get the BPI Web Feed

Using the HTML code below, you can display this Business Process Incubator page content with the current filter and sorting inside your web site for FREE.

Copy/Paste this code in your website html code:

<iframe src="https://www.businessprocessincubator.com/content/where-did-i-go-wrong-explaining-errors-in-process-models/?feed=html" frameborder="0" scrolling="auto" width="100%" height="700">

Customizing your BPI Web Feed

You can click on the Get the BPI Web Feed link on any of our page to create the best possible feed for your site. Here are a few tips to customize your BPI Web Feed.

Customizing the Content Filter
On any page, you can add filter criteria using the MORE FILTERS interface:

Customizing the Content Filter

Customizing the Content Sorting
Clicking on the sorting options will also change the way your BPI Web Feed will be ordered on your site:

Get the BPI Web Feed

Some integration examples

BPMN.org

XPDL.org

×