In this paper, we describe the modeling and analysis of a protocol for operational support during workflow enactment. Operational support provides online replies to questions such as "is my execution valid?" and "how do I end the execution in the fastest/cheapest way?", and may be invoked multiple times for each execution.
Multiple applications (operational support providers) may be able to answer such questions, so a protocol supporting this should be able to handle multiple providers, maintain data between queries about the same execution, and discard information when it is no longer needed.
We present a coloured Petri net model of a protocol satisfying our requirements. The model is used both to make our requirements clear by building a model-based prototype before implementation and to verify that the devised protocol is correct.
We present techniques to make analysis of the large state-space of the model possible, including modeling techniques and an improved state representation for coloured Petri nets allowing explicit representation of state spaces with more than 108 states on a normal PC.
We briefly describe our implementation in the process mining tool ProM and how we have used it to improve an existing provider.
|Title of host publication||Applications and Theory of Petri Nets (32nd International Conference, PETRI NETS 2011, Newcastle, UK, June 20-24, 2011. Proceedings)|
|Editors||L.M. Kristensen, L. Petrucci|
|Place of Publication||Berlin|
|Publication status||Published - 2011|
|Name||Lecture Notes in Computer Science|