Formal Modeling and Verification of Property-based Resource Consumption Cycles

Document Type

Conference Proceeding

Source of Publication

2021 IEEE International Conference on Services Computing (SCC)

Publication Date

1-10-2021

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.

ISBN

9781665416832

Publisher

Institute of Electrical and Electronics Engineers (IEEE)

Volume

00

Disciplines

Computer Sciences

Keywords

Computational modeling, Conferences, Automata, Service computing, Information systems, Formal verification

Indexed in Scopus

no

Open Access

no

Link to Full Text

Share

COinS