Modeling and verification of a protocol for operational support using coloured Petri nets

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.