Modellazione dei processi aziendali - Methods for the specification and verification of business processes

MPB 2013/14 (295AA / 372AA, 6 CFU)

Lecturer: Roberto Bruni (web - CLI - email - phone 050 2212785 - fax 050 2212726)

Question time: Thursday 15:00-17: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.


Tool(s) 188072_149141125103453_6888195_q.jpg

Woflan: a Petri-net-based Workflow Analyzer

Woped: Workflow Petri Net Designer

yEd: Graph Editor

Yaoqiang BPMN Editor: BPMN Editor


Bizagi Process Modeler: BPMN editor

Visual Paradigm offers University of Pisa VP-UML, Logizian for educational use through the VP Academic Partner Program.


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 wednesday November 6, 14:00-16:00 in Room A1.

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.


N Date Time Room Lecture notes Topics Links
1 Wed 25/09 16-18 N1 Lecture 1 Course introduction: course objectives, textbooks,
BPM aim and motivation, models and abstraction
2 Fri 27/09 11-13 L1 Lecture 2 Introduction to Business Processes: work units, processes,
terminology, organizational structures, process management
3 Wed 02/10 16-18 N1 Examples Examples and Exercises
4 Fri 04/10 11-13 L1 Lecture 3 Business Processes Lifecyle: design and analysis,
configuration, enactment, evaluation,
administration and stakeholders
5 Wed 09/10 16-18 N1 Lecture 4 Business Process Methodology:
levels of business processes, business strategies,
operational goals, organizational BP, operational BP,
implemented BP, strategy and organization,
BP methodology
6 Fri 11/10 11-13 L1 Lecture 5 (updated 11 Oct.)
Lecture 6
Evolution of Enterprise Systems Architectures:
separation of concerns, individual enterprise applications,
siloed EA, EA integration, value chains and process orientation,
workflow management coalition, enterprise service computing

Business Process Modelling Abstractions:
conceptual model, horizontal abstraction,
aggregation abstraction, vertical abstraction,
from value systems to BP implementation
7 Wed 16/10 14-16 N1 Lecture 7
Notation A* (uploaded 22 Oct.)
Introduction to Petri nets:
from finite state automata to Petri nets,
multisets and markings
8 Fri 18/10 11-13 L1 Lecture 8 (updated 16 Oct.)
Reachable marking (uploaded 22 Oct.)
More concepts about Petri nets:
transition enabling and firing, firing sequences,
reachable markings, occurrence graph
9 Wed 23/10 14-16 N1 Exercises (from Lecture 8) Examples and Exercises
10 Fri 25/10 11-13 L1 Behavioural and structural properties
(informally, from Lecture 8)
Behavioural properties, formally
Lecture 9
Net properties overview:
liveness, deadlock freedom, boundedness, safeness,
cyclicity, place liveness, weak and strong connectedness,
S-systems, T-systems, free-choice nets

Nets as matrices: incidence matrices,
markings as vectors, Parikh vectors,
marking equation lemma, monotonicity lemma
11 Wed 30/10 14-17 N1 Lecture 10
S-invariants, fundamental property of S-invariants,
alternative characterization, support, positive S-invariants,
about boundedness, reachability and liveness,
T-invariants, fundamental property of T-invariants,
alternative characterization, reproduction lemma,
about liveness and boundedness
12 Fri 01/11 11-13 L1 Holiday
13 Wed 06/11 14-16 A1 Mid-Term Exam
14 Fri 08/11 11-13 L1 Holiday
15 Wed 13/11 14-17 N1 Solutions to exercises
T-invariants (from Lecture 10)
Lecture 11
Lecture 12
Properties as invariants:
liveness, deadlock freedom, boundedness

Other properties:
boundedness lemma, exchange lemmas, connectedness theorems

Workflow nets:
definition, control flow aspects, decorations
16 Fri 15/11 11-13 L1 Lecture 13
Lecture 14
Analysis of workflow nets:
structural analysis, activity analysis, token analysis,
net analysis, verification and validation,
reachability analysis, coverability graph,
soundness, reset transition, main soundness theorem

Workflow nets:
soundness (and safeness) by construction
17 Wed 20/11 14-16 N1 Lecture 15 S-systems:
fundamental property of S-systems, S-invariants of S-nets,
reachability lemma for S-nets, liveness theorem,
reachability theorem, boundedness theorem

circuits and token count on a circuit,
fundamental property of T-systems, 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
18 Fri 22/11 11-13 L1 Exercises
Lecture 16
Free-choice nets:
Fundamental property of free-choice nets,
clusters, fundamental property of clusters in f.c. nets,
stability, siphons, proper siphon,
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
19 Wed 27/11 14-17 N1 Free-choice nets (from Lecture 16)
Lecture 17
Lecture 18
Free-choice nets:
Commoner's theorem, complexity issues, rank theorem, S-cover, T-cover

Diagnosis of Workflow nets:
Woped, Woflan, TP-handles, PT-handles, well-handled nets,
well-structured workflow netsnets, error sequences,
non-live sequences, unbounded sequences

Workflow systems:
workflow modules, strong and weak structural compatibility,
workflow system, weak soundness
20 Fri 29/11 - - Canceled
21 Wed 04/12 14-17 N1 Lecture 19 EPC:
22 Fri 06/12 11-13 L1 Lecture 20
Lecture 21

Workflow patterns:
23 Wed 11/12 14-16 N1 Lecture 22
Lecture 23

24 Fri 13/12 11-13 L1 Lecture 24 Process mining:

magistraleinformaticaeconomia/mpb/2013-14/start.txt · Ultima modifica: 10/09/2014 alle 10:23 (9 anni fa) da Roberto Bruni