Formal Modeling and Verification of Property-based Resource Consumption Cycles
Source of Publication
2021 IEEE International Conference on Services Computing (SCC)
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.
Institute of Electrical and Electronics Engineers (IEEE)
Computational modeling, Conferences, Automata, Service computing, Information systems, Formal verification
Halima, Rania Ben; Klai, Kais; Sellami, Mohamed; and Maamar, Zakaria, "Formal Modeling and Verification of Property-based Resource Consumption Cycles" (2021). All Works. 4689.
Indexed in Scopus