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

Document Type

Conference Proceeding

Source of Publication

Communications in Computer and Information Science

Publication Date

1-1-2018

Abstract

© 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.

ISBN

9783030028510

ISSN

1865-0929

Publisher

Springer Verlag

Volume

929

First Page

40

Last Page

49

Disciplines

Business

Keywords

Business process, Cloud resource, Formal verification, Temporal properties

Scopus ID

85055808888

Indexed in Scopus

yes

Open Access

no

Link to Full Text

Share

COinS