Description of TUTORIAL

We discovered a mismatch between verification and validation of even very simple business processes based on service composition and using semantic service specification. In more in-depth studies, we found that it is due to different business context of applying these services. Hence, we introduced semantic task specification for specifying tasks in their respective business context, where a specific semantic task specification may become a supertype of the corres­ponding semantic service specification, and this can be recursively applied to higher-level semantic task specifications in business processes.

Such semantic task specifications can be utilized for formal verification of traditionally represented business process models (e.g., through control flows defined in BPMN), where they semantically annotate the (BPMN) tasks. This verification through model checking determines whether time logic formulas specifying certain properties are violated (or not) in a behavioral business process model. It integrates object life cycle models with behavioral models derived from task-centric (BPMN) models, where the integration is done by use of semantic task specifications.

Formalizing business rules through properties referring to object life cycles rather than directly to task-centric models has the advantage of decoupling and potential reuse for several business models. In effect, this verification can show that a business rule is fulfilled and, indirectly, that the corresponding semantic task specifications correctly define their business context.


Submission Requirements

No submission is needed.

Facilitating individuals, their institutions and contact emails

Kaindl, Hermann,, TU Wien (TUW), Austria

The target audience is practitioners, students and educators.


The Tutorials will be held on June 10, at Stockholm University’s Kista campus.