Formal Modeling and Verification of Property-based Resource Consumption Cycles

Rania Ben Halima; Kais Klai; Mohamed Sellami; Zakaria Maamar

doi:10.1109/SCC53864.2021.00052

Formal Modeling and Verification of Property-based Resource Consumption Cycles

Rania Ben Halima
, Kais Klai
, Mohamed Sellami
, Zakaria Maamar

Institut Polytechnique de Paris
University Paris 13
Zayed University

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

3 Citations (Scopus)

Abstract

To respond to users' demands, organizations' in-formation systems are put into action consuming resources of different types. However, it happens that resources are poorly defined raising concerns about their availabilities at run-time. To ensure the correct definition of resources, this paper presents an approach to formally model and verify them using model-checking. First, properties referred to as limited, limited-but-renewable, and non-shareable are assigned to resources allowing to develop their consumption cycles. Afterwards, we model property-based resource consumption cycles as state diagrams and then, convert them into timed automata in preparation for their formal verification. After this conversion, specific CTL formulae are associated with each resource property. A case study illustrates how some cloud resources are defined as limited, shared, and even shared temporarily. These resources are modeled as timed automata and the conformity of their respective behaviors with respect to resource properties is verified.

Original language	English
Title of host publication	Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021
Editors	Barbara Carminati, Carl K. Chang, Ernesto Damiani, Deng Shuiguang, Wei Tan, Zhongjie Wang, Robert Ward, Jia Zhang
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	370-375
Number of pages	6
ISBN (Electronic)	9781665416832
DOIs	https://doi.org/10.1109/SCC53864.2021.00052
Publication status	Published - 1 Jan 2021
Event	2021 IEEE International Conference on Services Computing, SCC 2021 - Virtual, Online, United States Duration: 5 Sept 2021 → 11 Sept 2021

Publication series

Name	Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021

Conference

Conference	2021 IEEE International Conference on Services Computing, SCC 2021
Country/Territory	United States
City	Virtual, Online
Period	5/09/21 → 11/09/21

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Keywords

Model Checking
Re-source Consumption Cycle
Resource Management
Timed Automata
UPPAAL

Access to Document

10.1109/SCC53864.2021.00052

Cite this

Halima, R. B., Klai, K., Sellami, M., & Maamar, Z. (2021). Formal Modeling and Verification of Property-based Resource Consumption Cycles. In B. Carminati, C. K. Chang, E. Damiani, D. Shuiguang, W. Tan, Z. Wang, R. Ward, & J. Zhang (Eds.), Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021 (pp. 370-375). (Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/SCC53864.2021.00052

Halima, Rania Ben ; Klai, Kais ; Sellami, Mohamed et al. / Formal Modeling and Verification of Property-based Resource Consumption Cycles. Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021. editor / Barbara Carminati ; Carl K. Chang ; Ernesto Damiani ; Deng Shuiguang ; Wei Tan ; Zhongjie Wang ; Robert Ward ; Jia Zhang. Institute of Electrical and Electronics Engineers Inc., 2021. pp. 370-375 (Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021).

@inproceedings{da57da1292ce4a54b2a624d1508523f9,

title = "Formal Modeling and Verification of Property-based Resource Consumption Cycles",

abstract = "To respond to users' demands, organizations' in-formation systems are put into action consuming resources of different types. However, it happens that resources are poorly defined raising concerns about their availabilities at run-time. To ensure the correct definition of resources, this paper presents an approach to formally model and verify them using model-checking. First, properties referred to as limited, limited-but-renewable, and non-shareable are assigned to resources allowing to develop their consumption cycles. Afterwards, we model property-based resource consumption cycles as state diagrams and then, convert them into timed automata in preparation for their formal verification. After this conversion, specific CTL formulae are associated with each resource property. A case study illustrates how some cloud resources are defined as limited, shared, and even shared temporarily. These resources are modeled as timed automata and the conformity of their respective behaviors with respect to resource properties is verified.",

keywords = "Model Checking, Re-source Consumption Cycle, Resource Management, Timed Automata, UPPAAL",

author = "Halima, \{Rania Ben\} and Kais Klai and Mohamed Sellami and Zakaria Maamar",

note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 2021 IEEE International Conference on Services Computing, SCC 2021 ; Conference date: 05-09-2021 Through 11-09-2021",

year = "2021",

month = jan,

day = "1",

doi = "10.1109/SCC53864.2021.00052",

language = "English",

series = "Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "370--375",

editor = "Barbara Carminati and Chang, \{Carl K.\} and Ernesto Damiani and Deng Shuiguang and Wei Tan and Zhongjie Wang and Robert Ward and Jia Zhang",

booktitle = "Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021",

}

Halima, RB, Klai, K, Sellami, M & Maamar, Z 2021, Formal Modeling and Verification of Property-based Resource Consumption Cycles. in B Carminati, CK Chang, E Damiani, D Shuiguang, W Tan, Z Wang, R Ward & J Zhang (eds), Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021. Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021, Institute of Electrical and Electronics Engineers Inc., pp. 370-375, 2021 IEEE International Conference on Services Computing, SCC 2021, Virtual, Online, United States, 5/09/21. https://doi.org/10.1109/SCC53864.2021.00052

Formal Modeling and Verification of Property-based Resource Consumption Cycles. / Halima, Rania Ben; Klai, Kais; Sellami, Mohamed et al.
Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021. ed. / Barbara Carminati; Carl K. Chang; Ernesto Damiani; Deng Shuiguang; Wei Tan; Zhongjie Wang; Robert Ward; Jia Zhang. Institute of Electrical and Electronics Engineers Inc., 2021. p. 370-375 (Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021).

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

TY - GEN

T1 - Formal Modeling and Verification of Property-based Resource Consumption Cycles

AU - Halima, Rania Ben

AU - Klai, Kais

AU - Sellami, Mohamed

AU - Maamar, Zakaria

PY - 2021/1/1

Y1 - 2021/1/1

N2 - To respond to users' demands, organizations' in-formation systems are put into action consuming resources of different types. However, it happens that resources are poorly defined raising concerns about their availabilities at run-time. To ensure the correct definition of resources, this paper presents an approach to formally model and verify them using model-checking. First, properties referred to as limited, limited-but-renewable, and non-shareable are assigned to resources allowing to develop their consumption cycles. Afterwards, we model property-based resource consumption cycles as state diagrams and then, convert them into timed automata in preparation for their formal verification. After this conversion, specific CTL formulae are associated with each resource property. A case study illustrates how some cloud resources are defined as limited, shared, and even shared temporarily. These resources are modeled as timed automata and the conformity of their respective behaviors with respect to resource properties is verified.

AB - To respond to users' demands, organizations' in-formation systems are put into action consuming resources of different types. However, it happens that resources are poorly defined raising concerns about their availabilities at run-time. To ensure the correct definition of resources, this paper presents an approach to formally model and verify them using model-checking. First, properties referred to as limited, limited-but-renewable, and non-shareable are assigned to resources allowing to develop their consumption cycles. Afterwards, we model property-based resource consumption cycles as state diagrams and then, convert them into timed automata in preparation for their formal verification. After this conversion, specific CTL formulae are associated with each resource property. A case study illustrates how some cloud resources are defined as limited, shared, and even shared temporarily. These resources are modeled as timed automata and the conformity of their respective behaviors with respect to resource properties is verified.

KW - Model Checking

KW - Re-source Consumption Cycle

KW - Resource Management

KW - Timed Automata

KW - UPPAAL

U2 - 10.1109/SCC53864.2021.00052

DO - 10.1109/SCC53864.2021.00052

M3 - Conference contribution

AN - SCOPUS:85123299443

T3 - Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021

SP - 370

EP - 375

BT - Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021

A2 - Carminati, Barbara

A2 - Chang, Carl K.

A2 - Damiani, Ernesto

A2 - Shuiguang, Deng

A2 - Tan, Wei

A2 - Wang, Zhongjie

A2 - Ward, Robert

A2 - Zhang, Jia

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 2021 IEEE International Conference on Services Computing, SCC 2021

Y2 - 5 September 2021 through 11 September 2021

ER -

Halima RB, Klai K, Sellami M, Maamar Z. Formal Modeling and Verification of Property-based Resource Consumption Cycles. In Carminati B, Chang CK, Damiani E, Shuiguang D, Tan W, Wang Z, Ward R, Zhang J, editors, Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021. Institute of Electrical and Electronics Engineers Inc. 2021. p. 370-375. (Proceedings - 2021 IEEE International Conference on Services Computing, SCC 2021). doi: 10.1109/SCC53864.2021.00052

Formal Modeling and Verification of Property-based Resource Consumption Cycles

Abstract

Publication series

Conference

UN SDGs

Keywords

Access to Document

Fingerprint

Cite this