Title: Timed CTL checking of time critical cloud applications using timed bigraphs

Authors: Fateh Latreche; Faiza Belala

Addresses: LIRE Laboratory, Constantine 2, Abdelhamid Mehri University, Constantine, Algeria ' LIRE Laboratory, Constantine 2, Abdelhamid Mehri University, Constantine, Algeria

Abstract: Controlling cloud resources provisioning for time critical applications is crucial to meet required quality of service (QoS) of modern applications. Both computational resources capabilities and network bandwidth should be considered to accurately serve practical needs, while complying relevant constraints. The objective of this work is to show how to add time constructs to the bigraphical reactive systems (BRSs) formalism, in order to describe and analyse the execution of cloud applications having temporal constraints. In particular, we are interested in the cloud resource allocation problem to meet end user requests while considering network deadline, as well as the service processing time. The proposed time-aware BRS model is then integrated in the Real-Time Maude language and its TCTL model checker in order to obtain an executable and analysable specification of cloud applications having temporal constraints.

Keywords: time critical cloud applications; bigraphical reactive systems; BRSs; Real-Time Maude; TCTL model checking.

DOI: 10.1504/IJCCBS.2019.106818

International Journal of Critical Computer-Based Systems, 2019 Vol.9 No.4, pp.379 - 406

Received: 17 Sep 2018
Accepted: 30 Aug 2019
Published online: 21 Apr 2020 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article