The lecture introduces advanced topics in Business Process Management (BPM). In particular, the formal side of BPM is investigated. In the first part, we focus on the generic formalization aspects including syntax and semantics of process languages. Based thereon, basic notions for formal analysis of process models are investigated. Finally, a set of existing techniques for analyzing concrete properties is introduced.
How to formalize it | 01:32:33 | |
---|---|---|
Review | 00:14:19 | |
Operational Semantics | 00:14:12 | |
Formalization Principles | 00:18:57 | |
Conceptualization Principle | 00:14:13 | |
Semantics of Task Structures | 00:12:31 | |
Denotational Semantics | 00:12:15 |
Oryx Workshop | 01:12:56 | |
---|---|---|
Introduction | 00:06:49 | |
Architecture | 00:09:11 | |
Stencil Sets | 00:22:45 | |
Client Plugins | 00:10:00 | |
Server Plugins | 00:05:50 | |
Development Environment | 00:18:21 |
Temporal Logics | 01:27:35 | |
---|---|---|
Temporal Logics | 00:17:14 | |
Investigated paths | 00:14:44 | |
Semantic of Temporal Operators | 00:11:41 | |
Definition of Relation 1 | 00:14:04 | |
Definition of Relation 6 | 00:18:04 | |
Temporal Logic CTL | 01:28:00 |
States | 01:26:38 | |
---|---|---|
Introduction | 00:13:31 | |
Didactive Verification | 00:11:22 | |
Petri Net Process | 00:12:49 | |
Petri Net Example 2 | 00:12:13 | |
Kripke Structures | 00:09:22 | |
Definition of Path | 00:12:48 | |
State Space | 00:14:33 |
State Space Reduction Techniques to Verify Business Processes | 01:11:42 | |
---|---|---|
Correctness of Business Processes | 00:10:12 | |
State Space Explosion | 00:09:27 | |
Partial Order Reduction | 00:22:17 | |
Symmetry Reduction | 00:14:18 | |
Lessons Learned | 00:15:34 |
Compliance Checking | 01:23:11 | |
---|---|---|
Application: Compliance Checking | 00:22:50 | |
Reaction to new Compliance Rule | 00:10:34 | |
Expressing Compliance Rules as Queries | 00:06:54 | |
Final State Model Checking | 00:15:13 | |
Process Subject to Checking | 00:20:18 | |
Patterns and Anti Patterns | 00:07:22 |
Compliance Checking (2) | 01:06:39 | |
---|---|---|
Checking Rule | 00:11:02 | |
Anti Patterns | 00:09:17 | |
Matching Anti Patterns to Process | 00:10:15 | |
Representing Data Compliance | 00:11:46 | |
Data and Conditional Rules in BPMN-Q | 00:10:21 | |
Conditional Precedence | 00:13:58 |
Explicit vs. Symbolic Model Checking | 01:27:32 | |
---|---|---|
Modelling Process Overview | 00:11:08 | |
Next Steps | 00:05:36 | |
Büchi Automoton for Kripke Structure | 00:22:01 | |
Example | 00:15:19 | |
Immediate Acknowledgement | 00:23:23 | |
CTL Model Checking, Idea | 00:10:05 |
Introduction | 01:30:14 | |
---|---|---|
Organization | 00:11:16 | |
Introduction and Motivation | 00:17:10 | |
BPM Primer (1) | 00:21:08 | |
BPM Primer (4) | 00:19:40 | |
Syntax of Formalizations | 00:11:04 | |
Translations Semantics | 00:11:28 |