Formal Modelling of IT Resource Allocation in Business Processes

IT (Information Technology) takes part in virtually every aspect of BPM (Business Process Management). In fact, it would be unlikely for a modern organization not to use some IT resources, whether in the form of local computing or storage units, (web) services or even Cloud resources, for the execution of its business activities. Despite the wide range of use of IT resources in the context of BPM, the focus of researchers has been directed at human resources when dealing with the resource perspective in business processes. This results in a lack in explicit and formal description of IT resource management in the existing BPs. Besides the lack in formalization, the need for a verification method to check the correctness of IT resource allocations is still unquenched. In fact, without formal verification, the designer can easily model erroneous allocations which lead to runtime errors if left untreated at design-time. In this work, we address the above shortcomings by proposing a formal model for the IT resource perspective in BPs using the Coloured Petri Net formalism. We implemented our model using CPN Tools which we also used to check basic properties related to the well-construction of our model as well as to check the correctness of IT resource allocation at design-time.