Formal Modelling and Verification of Cloud Resource Allocation in Business Processes

Abstract

Cloud environments have been increasingly used by companies for deploying and executing business processes to enhance their performance while lowering the operating cost. Nevertheless, the combination of business processes and Cloud environments is a field that needs to be further studied since it lacks an explicit and formal description of the resource perspective in the existing business processes and especially of Cloud-related properties, namely vertical/horizontal elasticity. Therefore, this field cannot yet fully benefit of what Cloud environments can offer. Besides the lack in formalization, there is also a need for a verification method to check the correctness of allocations. 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 Cloud resource perspective in business processes using the Coloured Petri net formalism, which can be used to check the correctness of Cloud resource allocation at design-time.