Formal specification and verification of cloud resource allocation using timed petri-nets

Source of Publication

Communications in Computer and Information Science


© Springer Nature Switzerland AG 2018. Context: Known for its resource elasticity and pay-per-use model, more and more organizations are adopting cloud computing to support the execution of their business processes. To support organizations meet their financial restrictions, cloud providers offer different time-based pricing strategies. Objective: The proposed approach aims at assisting business process designers identify necessary cloud resources with respect to temporal and financial restrictions on business processes. The former minimizes the search time for cloud resources while the latter minimizes the cost of leasing these resources. Method: The proposed approach considers 2 inputs, a time-constrained business process specification and a list of allocated cloud resources, and then confirms whether this process has the necessary cloud resources, satisfies the temporal and financial restrictions, and is deadlock-free. To this end, the specification is automatically translated into a Temporal Petri-Net. Results: The implementation on a real case study has shown that the proposed approach ensures a proper matching between process activities and cloud resources.

Document Type

Conference Proceeding



First Page


Last Page


Publication Date