Strumenti Utente

Strumenti Sito


Methods for the specification and verification of business processes

MPB 2017/18 (295AA, 6 cfu)

part of Business Performance Analysis (APA 2017/18, 417AA, 12 cfu)

Lecturer: Roberto Bruni

Contact: web - email - phone 050 2212785 - fax 050 2212726

Question time: Wednesday 14:00-16:00 or by appointment


The course aims to reconcile abstraction techniques and high-level diagrammatic notations together with modular and structural approaches. The objective is to show the impact of the analysis and verification properties of business processes on the choice of the best suited specification and modelling languages. At the end of the course, the students will gain some familiarity with business process terminology, with different models and languages for the representation of business processes, with different kinds of logical properties that such models can satisfy and with different analysis and verification techniques. The students will also experiment with some tools for the design and analysis of business processes.

Course Overview

Business process management. Evolution of Enterprise Systems Architectures. Conceptual models and abstraction mechanisms. Petri nets: invariants, S-systems, T-systems, Free-choice systems and their properties. Workflow nets and workflow modules. Workflow patterns. Event-driven Process Chains (EPC). Business Process Modelling Notation (BPMN). Yet Another Workflow Language (YAWL). Business Process Execution Language (BPEL). Process Mining.


Quick reference(s)

Tool(s) 188072_149141125103453_6888195_q.jpg


The evaluation will be based on mid-term written exams, a group project and an oral exam. The final score will be obtained by combining the scores of the above exams with equal weight.

The mid-term exam will be held on: To be announced.
Registration to the exam is mandatory.

The student must demonstrate the ability to put into practice and to execute, with critical awareness, the activities illustrated or carried out under the guidance of the teacher during the course.


  • An additional lecture has been scheduled on tuesday 17/10 (16:00-18:00, room L1) to replace the one canceled on 6/10.
  • The lecture of friday 6/10 has been canceled because of the Internet Festival. If necessary it will be re-scheduled in the next weeks.
  • as the course starts:
    Each student should send an email to the professor from his/her favourite email account with subject MPB17 and the following data
    (by doing so, the account will be included in the class mailing-list, where important announcements can be sent):
    1. first name and last name (please clarify which is which, to avoid ambiguities)
    2. enrolment number (numero di matricola)
    3. bachelor degree (course of study and university)


N Date Time Room Lecture notes Topics Links
1 Wed 20/09 16:00-18:00 A1 Lecture 1 Course introduction:
course objectives, textbooks,
BPM aim and motivation,
models and abstraction
2 Fri 22/09 14:00-16:00 L1 Lecture 2 Introduction to Business Processes:
work units, processes, terminology,
organizational structures,
process management
3 Wed 27/09 16:00-18:00 A1 Examples Examples and Exercises
4 Fri 29/09 14:00-16:00 L1 Exercises
Lecture 3
Business Processes Lifecyle:
design and analysis, configuration,
enactment, evaluation,
administration and stakeholders
5 Wed 04/10 16:00-18:00 A1 Lecture 4
Lecture 5
Business Process Modelling Abstractions:
conceptual model, workflow management,
horizontal abstraction,
aggregation abstraction,
vertical abstraction,
value chains and value systems, Taylorism,
from business functions to processes

Business Process Methodology:
levels of business processes,
business strategies, operational goals,
organizational BP, operational BP,
implemented BP, design guidelines
# Fri 06/10 14:00-16:00 L1 Canceled Lecture canceled for allowing students to attend events of the Internet Festival
6 Wed 11/10 16:00-18:00 A1 Lecture 6
Lecture 7
Evolution of Enterprise Systems Architectures:
separation of concerns, sw architectures
individual enterprise applications,
enterprise resource planning system,
siloed enterprise applications,
enterprise application integration,
message-oriented middleware,
enterprise service computing

Introduction to Petri nets:
finite state automata
7 Fri 13/10 14:00-16:00 L1 Exercises (from Lecture 7)
Petri nets (from Lecture 7)
Lecture 8
Introduction to Petri nets:
from finite state automata to Petri nets

More concepts about Petri nets:
multisets and markings,
transition enabling and firing, firing sequences,
reachable markings, occurrence graph
8 Tue 17/10 16:00-18:00 L1 Exercises (from Lecture 7)
Exercises (from Lecture 8)
Modelling with Petri nets:
Examples and Exercises
9 Wed 18/10 16:00-18:00 A1 Lecture 9
Lecture 10 (1st part)
Behavioural properties:
liveness, place liveness, deadlock freedom,
boundedness, safeness, cyclicity

Structural properties:
weak and strong connectedness,
S-systems, T-systems, free-choice nets

Nets as matrices:
incidence matrices, markings as vectors,
Parikh vectors, marking equation lemma
10 Fri 20/10 14:00-16:00 L1 Exercises (from Lecture 9)
Lecture 10 (2nd part)
Lecture 11 (1st part)
Nets as matrices:
marking equation lemma (proof), monotonicity lemma,
boundedness lemma, repetition lemma

S-invariants, fundamental property of S-invariants,
alternative characterization of S-invariant
11 Wed 25/10 16:00-18:00 A1 Exercises (from Lecture 10)
Exercises (from Lecture 11)
Lecture 11 (2nd part)
Lecture 12
Lecture 13
support, positive S-invariants,
about boundedness, reachability and liveness,
T-invariants, fundamental property of T-invariants,
alternative characterization of T-invariants,
reproduction lemma,
about liveness and boundedness

Other properties of nets:
exchange lemmas, connectedness theorems
(their proofs are optional reading)

Workflow nets:
definition, control flow aspects, decorations
12 Fri 27/10 14:00-16:00 L1 Exercises (from Lecture 11)
Exercises (from Lecture 12)
Workflow nets (from Lecture 13)
Lecture 14
Workflow nets:
control flow aspects, triggers

Analysis of workflow nets:
structural analysis, activity analysis,
token analysis, net analysis,
verification and validation,
reachability analysis
13 Thu 02/11 14:00-16:00 A1 Mid-Term Exam Registration
(look at past exercises)
14 Solutions to mid-term exam
Exercises (from Lecture 13)
Coverability graph (from Lecture 14)
Soundness theorem (from Lecture 14)
Analysis of workflow nets:
coverability graph, soundness,
N*, soundness theorem
15 Exercises (from Lecture 14)
Lecture 15
Lecture 16
Lecture 17
Workflow nets:
soundness (and safeness) by construction

fundamental property of S-systems,
S-invariants of S-nets, liveness theorem
reachability lemma, reachability theorem,
boundedness theorem

circuits and token count on a circuit,
fundamental property of T-systems
16 Exercises (from Lectures 15, 16)
Analysis of T-system (from Lecture 17)
A note on P and NP (optional reading)
T-invariants of T-nets
liveness theorem,
boundedness theorem for live T-systems,
boundedness in strongly connected T-systems,
liveness in strongly connected T-systems
Exercises (from Lectures 17)
Lecture 18
Free-choice nets:
Fundamental property of free-choice nets,
clusters, fundamental property of clusters in f.c. nets,
stability, siphons, proper siphons,
fundamental property of siphons,
siphons and liveness, siphons and deadlock
traps, proper traps,
fundamental property of traps,
a sufficient condition for deadlock freedom,
place-liveness and liveness in f.c. nets,
non-liveness and unmarked siphons in f.c. nets,
Commoner's theorem, complexity issues
18 Exercises (from Lecture 18)
Rank Theorem (from Lecture 18)
S- and T-Covers (from Lecture 18)
Lecture 19
Free-choice nets:
Rank theorem, S-cover, T-cover

Diagnosis of Workflow nets:
Woped, Woflan, TP-handles, PT-handles,
well-handled nets, well-structured wf nets
19 Exercises (from Lectures 19)
Error sequences (from Lecture 19)
Lecture 20
Diagnosis of Workflow nets:
error sequences, non-live sequences,
unbounded sequences

Workflow systems:
workflow modules, strong and weak compatibility,
workflow system, weak soundness,
20 Exercises (from Lectures 19, 20)
LF,k-controllability (from Lecture 20)
Lecture 21
Workflow systems:

Notation, semantics ambiguities and problems,
corresponding split, matching split
21 EPC semantics (from Lecture 21)
Lecture 22
policies (wfa, fc, et), from EPC to nets,
relaxed soundness

Notation, swimlanes, flow objects
22 Exercises (from Lectures 21)
BPMN (from Lecture 22)
artefacts, connecting onjects,
conversations, choreographies, collaborations,
from BPMN to nets
23 Exercises (from Lectures 22)
From BPMN to nets (from Lecture 22)
Lecture 23
From BPMN to nets (ctd.)

BPEL structured constructs, links,
transition condition, join condition,
from BPEL to nets
24 Lecture 24
Lecture 25
Quantitative analysis:
Performance dimensions and objectives,
KPI, cyle time analysis, Little's law,
cost analysis

resource allocation, classification diagrams,
capacity planning, simulation parameters,
task durations, BIMP
25 Exercises (from Lectures 22, 24)
Lecture 26
Process mining:
Event logs, discovery, conformance,
enhancement, perspectives, play-in, play-out,
replay, overfitting, underfitting
alpha-algorithm, footprint matrix,
naive fitness, improved fitness

Past courses

magistraleinformaticaeconomia/mpb/start.txt · Ultima modifica: 19/10/2017 alle 11:27 (12 ore fa) da Roberto Bruni