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

Objectives

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.

Textbook(s)

Business Process Management: Concepts, Languages, Architectures (book, main reference)
Diagnosing workflow processes using Woflan (article, recommended reading)
Workflow Management: Models, Methods, and Systems (book, optional reading)
Free Choice Nets (book, optional reading)
Further bibliography and lecture notes will be indicated during the course.

Tool(s)

Woflan: a Petri-net-based Workflow Analyzer

Woped: Workflow Petri Net Designer

yEd: Graph Editor

Yaoqiang BPMN Editor: BPMN Editor

BPMS: 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.

Exams

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.

Lectures

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 Exercises	Invariants: 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	Woped
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 T-systems: 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	Woflan
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	BPMN: Workflow patterns:
23	Wed 11/12	14-16	N1	Lecture 22 Lecture 23	BPEL: YAWL:
24	Fri 13/12	11-13	L1	Lecture 24	Process mining:
end