Formal verification of time-aware cloud resource allocation in business process

Rania Ben Halima; Slim Kallel; Kais Klai; Walid Gaaloul; Mohamed Jmaiel

doi:10.1007/978-3-319-48472-3_23

Formal verification of time-aware cloud resource allocation in business process

Rania Ben Halima
, Slim Kallel
, Kais Klai
, Walid Gaaloul
, Mohamed Jmaiel

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Cloud computing has become an essential ingredient for any modern enterprise information systems infrastructure to effectively facilitate business-process execution with a low operating cost. Most of pricing strategies proposed by Cloud providers are based on temporal dimension. That is why time is considered one of the most important Cloud resources properties. In addition, activities in the business process are also constrained by hard timing requirements. Therefore, it is essential to ensure the matching between temporal constraints of both Cloud resources and business process activities. The aim of the present paper is to ensure a consistent time-aware Cloud resource allocation: we propose to formally specify temporal constraints on cloud resources and on process activities in business processes. This specification is translated to timed automata in order to formally validate the consistency of the timeaware Cloud resource allocation, and to analyze and check its correctness against business-process temporal constraints.

Original language	English
Title of host publication	On the Move to Meaningful Internet Systems
Subtitle of host publication	OTM 2016 Conferences - Confederated International Conferences: CoopIS, CandTC, and ODBASE 2016, Proceedings
Editors	Tharam Dillon, Christophe Debruyne, Declan Oâ’Sullivan, Herve Panetto, Eva Kuhn, Claudio Agostino Ardagna, Robert Meersman
Publisher	Springer Verlag
Pages	400-417
Number of pages	18
ISBN (Print)	9783319484716
DOIs	https://doi.org/10.1007/978-3-319-48472-3_23
Publication status	Published - 1 Jan 2016
Event	Confederated International Conference On the Move to Meaningful Internet Systems, OTM 2016 held in conjunction with Conferences on CoopIS, CandTC and ODBASE 2016 - Rhodes, Greece Duration: 24 Oct 2016 → 28 Oct 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10033 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Confederated International Conference On the Move to Meaningful Internet Systems, OTM 2016 held in conjunction with Conferences on CoopIS, CandTC and ODBASE 2016
Country/Territory	Greece
City	Rhodes
Period	24/10/16 → 28/10/16

Keywords

Business process
Cloud resource
Cost
Formal verification
Temporal constraints

Access to Document

10.1007/978-3-319-48472-3_23

Cite this

Ben Halima, R., Kallel, S., Klai, K., Gaaloul, W., & Jmaiel, M. (2016). Formal verification of time-aware cloud resource allocation in business process. In T. Dillon, C. Debruyne, D. Oâ’Sullivan, H. Panetto, E. Kuhn, C. A. Ardagna, & R. Meersman (Eds.), On the Move to Meaningful Internet Systems: OTM 2016 Conferences - Confederated International Conferences: CoopIS, CandTC, and ODBASE 2016, Proceedings (pp. 400-417). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10033 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-48472-3_23

Ben Halima, Rania ; Kallel, Slim ; Klai, Kais et al. / Formal verification of time-aware cloud resource allocation in business process. On the Move to Meaningful Internet Systems: OTM 2016 Conferences - Confederated International Conferences: CoopIS, CandTC, and ODBASE 2016, Proceedings. editor / Tharam Dillon ; Christophe Debruyne ; Declan Oâ’Sullivan ; Herve Panetto ; Eva Kuhn ; Claudio Agostino Ardagna ; Robert Meersman. Springer Verlag, 2016. pp. 400-417 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ad5dc547747746cdba8d2b2238284c14,

title = "Formal verification of time-aware cloud resource allocation in business process",

abstract = "Cloud computing has become an essential ingredient for any modern enterprise information systems infrastructure to effectively facilitate business-process execution with a low operating cost. Most of pricing strategies proposed by Cloud providers are based on temporal dimension. That is why time is considered one of the most important Cloud resources properties. In addition, activities in the business process are also constrained by hard timing requirements. Therefore, it is essential to ensure the matching between temporal constraints of both Cloud resources and business process activities. The aim of the present paper is to ensure a consistent time-aware Cloud resource allocation: we propose to formally specify temporal constraints on cloud resources and on process activities in business processes. This specification is translated to timed automata in order to formally validate the consistency of the timeaware Cloud resource allocation, and to analyze and check its correctness against business-process temporal constraints.",

keywords = "Business process, Cloud resource, Cost, Formal verification, Temporal constraints",

author = "\{Ben Halima\}, Rania and Slim Kallel and Kais Klai and Walid Gaaloul and Mohamed Jmaiel",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; Confederated International Conference On the Move to Meaningful Internet Systems, OTM 2016 held in conjunction with Conferences on CoopIS, CandTC and ODBASE 2016 ; Conference date: 24-10-2016 Through 28-10-2016",

year = "2016",

month = jan,

day = "1",

doi = "10.1007/978-3-319-48472-3\_23",

language = "English",

isbn = "9783319484716",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "400--417",

editor = "Tharam Dillon and Christophe Debruyne and Declan O{\^a}{\textquoteright}Sullivan and Herve Panetto and Eva Kuhn and Ardagna, \{Claudio Agostino\} and Robert Meersman",

booktitle = "On the Move to Meaningful Internet Systems",

}

Ben Halima, R, Kallel, S, Klai, K, Gaaloul, W & Jmaiel, M 2016, Formal verification of time-aware cloud resource allocation in business process. in T Dillon, C Debruyne, D Oâ’Sullivan, H Panetto, E Kuhn, CA Ardagna & R Meersman (eds), On the Move to Meaningful Internet Systems: OTM 2016 Conferences - Confederated International Conferences: CoopIS, CandTC, and ODBASE 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10033 LNCS, Springer Verlag, pp. 400-417, Confederated International Conference On the Move to Meaningful Internet Systems, OTM 2016 held in conjunction with Conferences on CoopIS, CandTC and ODBASE 2016, Rhodes, Greece, 24/10/16. https://doi.org/10.1007/978-3-319-48472-3_23

Formal verification of time-aware cloud resource allocation in business process. / Ben Halima, Rania; Kallel, Slim; Klai, Kais et al.
On the Move to Meaningful Internet Systems: OTM 2016 Conferences - Confederated International Conferences: CoopIS, CandTC, and ODBASE 2016, Proceedings. ed. / Tharam Dillon; Christophe Debruyne; Declan Oâ’Sullivan; Herve Panetto; Eva Kuhn; Claudio Agostino Ardagna; Robert Meersman. Springer Verlag, 2016. p. 400-417 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10033 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Formal verification of time-aware cloud resource allocation in business process

AU - Ben Halima, Rania

AU - Kallel, Slim

AU - Klai, Kais

AU - Gaaloul, Walid

AU - Jmaiel, Mohamed

N1 - Publisher Copyright: © Springer International Publishing AG 2016.

PY - 2016/1/1

Y1 - 2016/1/1

N2 - Cloud computing has become an essential ingredient for any modern enterprise information systems infrastructure to effectively facilitate business-process execution with a low operating cost. Most of pricing strategies proposed by Cloud providers are based on temporal dimension. That is why time is considered one of the most important Cloud resources properties. In addition, activities in the business process are also constrained by hard timing requirements. Therefore, it is essential to ensure the matching between temporal constraints of both Cloud resources and business process activities. The aim of the present paper is to ensure a consistent time-aware Cloud resource allocation: we propose to formally specify temporal constraints on cloud resources and on process activities in business processes. This specification is translated to timed automata in order to formally validate the consistency of the timeaware Cloud resource allocation, and to analyze and check its correctness against business-process temporal constraints.

AB - Cloud computing has become an essential ingredient for any modern enterprise information systems infrastructure to effectively facilitate business-process execution with a low operating cost. Most of pricing strategies proposed by Cloud providers are based on temporal dimension. That is why time is considered one of the most important Cloud resources properties. In addition, activities in the business process are also constrained by hard timing requirements. Therefore, it is essential to ensure the matching between temporal constraints of both Cloud resources and business process activities. The aim of the present paper is to ensure a consistent time-aware Cloud resource allocation: we propose to formally specify temporal constraints on cloud resources and on process activities in business processes. This specification is translated to timed automata in order to formally validate the consistency of the timeaware Cloud resource allocation, and to analyze and check its correctness against business-process temporal constraints.

KW - Business process

KW - Cloud resource

KW - Cost

KW - Formal verification

KW - Temporal constraints

U2 - 10.1007/978-3-319-48472-3_23

DO - 10.1007/978-3-319-48472-3_23

M3 - Conference contribution

AN - SCOPUS:84995916471

SN - 9783319484716

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 400

EP - 417

BT - On the Move to Meaningful Internet Systems

A2 - Dillon, Tharam

A2 - Debruyne, Christophe

A2 - Oâ’Sullivan, Declan

A2 - Panetto, Herve

A2 - Kuhn, Eva

A2 - Ardagna, Claudio Agostino

A2 - Meersman, Robert

PB - Springer Verlag

T2 - Confederated International Conference On the Move to Meaningful Internet Systems, OTM 2016 held in conjunction with Conferences on CoopIS, CandTC and ODBASE 2016

Y2 - 24 October 2016 through 28 October 2016

ER -

Ben Halima R, Kallel S, Klai K, Gaaloul W, Jmaiel M. Formal verification of time-aware cloud resource allocation in business process. In Dillon T, Debruyne C, Oâ’Sullivan D, Panetto H, Kuhn E, Ardagna CA, Meersman R, editors, On the Move to Meaningful Internet Systems: OTM 2016 Conferences - Confederated International Conferences: CoopIS, CandTC, and ODBASE 2016, Proceedings. Springer Verlag. 2016. p. 400-417. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-48472-3_23

Formal verification of time-aware cloud resource allocation in business process

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this