Indice
Modellazione dei processi aziendali - Methods for the specification and verification of business processes
MPB 2014/15 (295AA / 372AA, 6 CFU)
Lecturer: Roberto Bruni
Contact: web - CLI - 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.
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 Friday 07/11 from 11:00 to 13:00 in room C1.
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 24/09 | 14-16 | N1 | Lecture 1 | Course introduction: course objectives, textbooks, BPM aim and motivation, models and abstraction | |
| 2 | Fri 26/09 | 11-13 | L1 | Lecture 2 | Introduction to Business Processes: work units, processes, terminology, organizational structures, process management | |
| 3 | Wed 01/10 | 14-16 | N1 | Examples | Examples and Exercises | |
| 4 | Fri 03/10 | 11-13 | L1 | Lecture 3 Lecture 4 | Business Processes Lifecyle: design and analysis, configuration, enactment, evaluation, administration and stakeholders Business Process Methodology: levels of business processes, business strategies, operational goals, organizational BP, operational BP, implemented BP, strategy and organization, BP methodology | |
| 5 | Wed 08/10 | 14-16 | N1 | Lecture 5 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 | |
| 6 | Fri 10/10 | 11-13 | L1 | Lecture 7 | Introduction to Petri nets: from finite state automata to Petri nets, multisets and markings More concepts about Petri nets: transition enabling and firing, firing sequences | Woped |
| 7 | Wed 15/10 | 14-16 | N1 | Exercises (from Lecture 7) Lecture 8 (updated 14/10/2014) | More concepts about Petri nets (from Lecture 8): firing sequences, reachable markings, occurrence graph Behavioural properties: liveness, deadlock freedom | |
| 8 | Fri 17/10 | 11-13 | L1 | Canceled | Lecture canceled due to a strike of the personnel of Polo Fibonacci | |
| 9 | Wed 22/10 | 14-16 | N1 | Exercises (from Lecture 8) Behavioural properties (from Lecture 8) | Examples and Exercises Behavioural properties: boundedness, safeness | |
| 10 | Fri 24/10 | 11-13 | L1 | Behavioural properties (from Lecture 8) Structural properties (from Lecture 8) Lecture 9 | Behavioural properties: cyclicity, place liveness 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, monotonicity lemma, boundedness lemma, repetition lemma | |
| 11 | Wed 29/10 | 14-16 | N1 | Lecture 10 Exercises (from Lecture 8) | 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 31/10 | 11-13 | L1 | Exercises (from Lecture 10) Lecture 11 (updated 30/10/14) Lecture 12 | Properties as invariants: liveness, deadlock freedom, boundedness Other properties: exchange lemmas, connectedness theorems Workflow nets: definition, control flow aspects, decorations | |
| 13 | Fri 07/11 | 11-13 | C1 | Mid-Term Exam | Registration | |
| 14 | Wed 12/11 | 14-16 | N1 | Solutions to mid-term exam Exercises (from Lecture 11) Triggers (from Lecture 12) Lecture 13 | Workflow nets: triggers Analysis of workflow nets: structural analysis, activity analysis, token analysis, net analysis, verification and validation, reachability analysis, coverability graph, soundness | |
| 15 | Fri 14/11 | 11-13 | L1 | Exercises (from Lectures 12) Soundness theorem (from Lecture 13) Lecture 14 Lecture 15 (updated 19/11/2014) | Analysis of workflow nets: soundness, reset transition, main soundness theorem Workflow nets: soundness (and safeness) by construction S-systems: fundamental property of S-systems, S-invariants of S-nets, liveness theorem | |
| 16 | Wed 19/11 | 14-16 | N1 | Exercises (from Lectures 13, 14) S-systems: Reachability theorem (from Lecture 15) T-systems (from Lecture 15) | S-systems: 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, liveness theorem, boundedness theorem for live T-systems, boundedness in strongly connected T-systems, liveness in strongly connected T-systems | |
| 17 | Fri 21/11 | 11-13 | L1 | Exercises (from Lecture 15) 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, Commoner's theorem, complexity issues | |
| 18 | Wed 26/11 | 14-16 | N1 | Exercises (from Lecture 16) Free-choice nets (from Lecture 16) Lecture 17 | Free-choice nets: Rank theorem, S-cover, T-cover Diagnosis of Workflow nets: Woped, Woflan, TP-handles, PT-handles, well-handled nets, well-structured workflow nets, error sequences, non-live sequences, unbounded sequences | Woflan ProM |
| 19 | Fri 28/11 | 11-13 | L1 | Exercises (from Lectures 16, 17) Lecture 18 Lecture 19 (updated 28/11/2014) | Workflow systems: workflow modules, strong and weak structural compatibility, workflow system, weak soundness EPC: Notation, semantics ambiguities and problems, corresponding split, matching split, policies (wfa, fc, et) | |
| 20 | Wed 3/12 | 14-17 | N1 | Exercises (from Lectures 18, 19) From EPC to nets (from Lecture 19) Lecture 20 | EPC: From EPC to nets, relaxed soundness BPMN: Notation, advanced constructs, conversations, choreographies, collaborations | yEd Yaoqiang BPMS Bizagi Logizian |
| 21 | Fri 5/12 | 11-13 | L1 | Exercises (from Lectures 19, 20) From BPMN to nets (from Lecture 20) Lecture 21 | BPMN: From BPMN to nets BPEL: WSDL | |
| 22 | Wed 10/12 | 14-17 | N1 | Exercises (from Lecture 20) From BPEL to nets (from Lecture 21) Lecture 24 (updated 10/12/2014) Lecture 25 | BPEL: BPEL structured constructs, links, transition condition, join condition, from BPEL to nets Quantitative analysis: Performance dimensions, performance objectives, KPI, cyle time analysis, Little's law, cost analysis, resource allocation, classification diagrams, capacity planning Simulation: simulation parameters, task durations, BIMP | BPEL2PNML BPEL2oWFN Woped BIMP |
| 23 | Fri 12/12 | 11-13 | L1 | Canceled | Lecture canceled due to a strike of the personnel of Polo Fibonacci | |
| 24 | Mon 15/12 | 11-13 | V1 | Exercises (from Lecture 24) Lecture 22 Lecture 23 Lecture 26 (until naive fitness, included) | Workflow patterns: basic patterns, advanced patterns, structural patterns, multiple instances, state-based patterns, cancellation patterns YAWL: notation, informal expressiveness Process mining: Event logs, discovery, conformance, enhancement, perspectives, play-in, play-out, replay, overfitting, underfitting, alpha-algorithm, footprint matrix, naive fitness | YAWL ProM |
| end |