Indice

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

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

MPB 2015/16 (295AA / 372AA, 6 CFU)

Lecturer: Roberto Bruni

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

Question time: Wednesday 16:00-18: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 on BPM, main reference)
Diagnosing workflow processes using Woflan (article on Formal Analysis of Workflows, recommended reading)
Workflow Management: Models, Methods, and Systems (book on Workflow Management, optional reading)
Free Choice Nets (book on Petri nets, optional reading)
Fundamentals of Business Process Management (book on BPMN, optional reading)
Process Mining (book on Process Mining, optional reading)
Further bibliography and lecture notes will be indicated during the course.

Quick reference(s)

Petri Nets World
PNML (Petri Nets Markup Language): XML-based standard for Petri nets
BPMN: Current specification v2.0
BPEL
Workflow Patterns
Process Mining
XES (eXtensible Event Stream): XML-based standard for event logs

Tool(s)

Woped: Workflow Petri Net Designer
Woflan: a Petri-net-based Workflow Analyzer (Windows only), also available as a ProM plugin (all platforms)
yEd: Graph Editor
Yaoqiang BPMN Editor: BPMN Editor
BPMS: Intalio BPMN Editor
Bizagi Process Modeler: BPMN editor (Windows only)
Visual Paradigm offers University of Pisa VP-UML, Logizian for educational use through the VP Academic Partner Program.
YAWL: Yet Another Workflow Language platform
ProM: Process Mining Framework
BIMP: Business Process Simulator

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: to be announced.

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.

Announcements

10/12/2015 (Project assignment):
You can require the final project by dropping an email to teacher with subject “[MBP15] Project request” and body containing the list of max 2 students who form the group to which the project will be assigned (first name, last name, student id number, email address). You will receive the project assignment and additional instructions in reply and will have about three weeks (a few days more if vacations are included in the period) to complete the project and write a short report about your work.

25/11/2015:
The results of the mid-term exam held on 5/11 are available through the exams registration portal.

21/10/2015:
The mid-term exam has been scheduled on Thursday 05/11/2015 (Room C1, 14:00-16:00).
Registration to the exam is mandatory.

21/10/2015:
An additional lecture has been scheduled on Monday 26/10/2015.
See the timetable below.

18/10/2015:
The additional lecture scheduled on Monday 19/10/2015 is canceled.

01/10/2015:
Two additional lectures have been scheduled on Monday 05/10/2015 and Monday 19/10/2015.
See the timetable below.

10/09/2015:
The first two lectures of Wednesday 23/09/2015 and Friday 25/09/2015 are canceled.
To recover, two additional lectures will be scheduled in October.
The course will start on Wednesday 30/09/2015.

as the course starts:
Each student should send an email to the professor from his/her favourite email account with subject MPB15 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)

Lectures

N	Date	Time	Room	Lecture notes	Topics	Links
1	Wed 23/09	14-16		Canceled	Lecture canceled due to teacher's travel commitments
2	Fri 25/09	11-13		Canceled	Lecture canceled due to teacher's travel commitments
3	Wed 30/09	14-16	N1	Lecture 1	Course introduction: course objectives, textbooks, BPM aim and motivation, models and abstraction
4	Fri 02/10	11-13	L1	Lecture 2	Introduction to Business Processes: work units, processes, terminology, organizational structures, process management
5	Mon 05/10	14-16	N1	Examples	Examples and Exercises
6	Wed 07/10	14-16	N1	Exercises Lecture 3	Business Processes Lifecyle: design and analysis, configuration, enactment, evaluation, administration and stakeholders
7	Fri 09/10	11-13	L1	Lecture 4 Lecture 5	Business Process Methodology: levels of business processes, business strategies, operational goals, organizational BP, operational BP, implemented BP, strategy and organization, BP methodology 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
8	Wed 14/10	14-16	N1	Lecture 6 Lecture 7 (updated 14/10/15)	Business Process Modelling Abstractions: conceptual model, horizontal abstraction, aggregation abstraction, vertical abstraction, from value systems to BP implementation Introduction to Petri nets: from finite state automata to Petri nets
9	Fri 16/10	11-13	L1	Exercises (from Lecture 7) Lecture 8	More concepts about Petri nets: multisets and markings, transition enabling and firing, firing sequences, reachable markings, occurrence graph	Woped
10	Wed 21/10	14-16	N1	Exercises (from Lecture 8) Behavioural properties (from Lecture 8) Structural properties (from Lecture 8)	Behavioural properties: liveness, place liveness, deadlock freedom, boundedness, safeness, cyclicity Structural properties: weak and strong connectedness, S-systems, T-systems, free-choice nets
11	Fri 23/10	11-13	L1	Exercises (from Lecture 8) Lecture 9	Nets as matrices: incidence matrices, markings as vectors, Parikh vectors, marking equation lemma, monotonicity lemma, boundedness lemma, repetition lemma
12	Mon 26/10	14-16	N1	Lecture 10 (updated 24/10/2015)	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
13	Wed 28/10	14-16	N1	Pisa CoderDojo Exercises (from Lecture 10) Lecture 11 Lecture 12	Other properties of nets: properties as invariants, exchange lemmas, connectedness theorems Workflow nets: definition, control flow aspects, decorations, triggers
14	Fri 30/10	11-13	L1	Exercises (from Lectures 11, 12) Lecture 13	Analysis of workflow nets: structural analysis, activity analysis, token analysis, net analysis, verification and validation, reachability analysis, coverability graph, soundness, N*
15	Thu 05/11	11-13	C	Mid-Term Exam	Registration (look at past exercises)
16	Wed 11/11	14-16	N1	Solutions to mid-term exam Exercises (from Lecture 13) Soundness theorem (from Lecture 13) Lecture 14	Analysis of workflow nets: soundness theorem Workflow nets: soundness (and safeness) by construction
17	Fri 13/11	11-13	L1	Exercises (from Lectures 13, 14) Lecture 15 Lecture 16	S-systems: fundamental property of S-systems, S-invariants of S-nets, liveness theorem reachability lemma, reachability theorem, boundedness theorem T-systems: circuits and token count on a circuit, fundamental property of T-systems, T-invariants of T-nets
18	Wed 18/11	14-16	N1	Exercises (from Lecture 15) Behavioural properties of T-systems (from Lecture 16) Lecture 17	T-systems: liveness theorem, boundedness theorem for live T-systems, boundedness in strongly connected T-systems, liveness in strongly connected T-systems 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
19	Fri 20/11	11-13	L1	Exercises (from Lectures 16, 17) Free-choice nets ctd. (from Lecture 17)	Free-choice nets: 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 Rank theorem, S-cover, T-cover
20	Wed 25/11	14-16	N1	Exercises (from Lecture 17) Lecture 18	Diagnosis of Workflow nets: Woped, Woflan, TP-handles, PT-handles, well-handled nets, well-structured wf nets, error sequences, non-live sequences, unbounded sequences	Woflan ProM
21	Fri 27/11	11-13	L1	Exercises (from Lectures 18) Lecture 19 Lecture 20	Workflow systems: workflow modules, strong and weak compatibility, workflow system, weak soundness EPC: Notation, semantics ambiguities and problems
22	Wed 02/12	14-16	N1	Exercises (from Lectures 19, 20) From EPC to nets (from Lecture 20)	EPC: corresponding split, matching split, policies (wfa, fc, et), from EPC to nets, relaxed soundness
23	Fri 04/12	L1	11-13	Lecture 21	BPMN: Notation, advanced constructs, conversations, choreographies, collaborations	yEd Yaoqiang BPMS Bizagi Logizian
24	Wed 09/12	N1	14-16	Exercises (from Lectures 20, 21) From BPMN to nets (from Lecture 21) Lecture 22	BPMN: From BPMN to nets Quantitative analysis: Performance dimensions and objectives, KPI, cyle time analysis, Little's law, cost analysis
25	Fri 11/12	L1	11-13	Exercises (from Lectures 21, 22) Resource allocation (from Lecture 22) Lecture 23 Lecture 24	Quantitative analysis: resource allocation, classification diagrams, capacity planning Simulation: simulation parameters, task durations, BIMP Process mining: Event logs, discovery, conformance, enhancement, perspectives, play-in, play-out, replay, overfitting, underfitting, alpha-algorithm, footprint matrix, naive fitness, improved fitness	Woped BIMP ProM
end

DidaWiki