Cellular access networks are essential for modern communication, evolving through successive generations to meet the increasing performance demands. As these networks become more complex, ensuring reliable and uninterrupted operation is a significant challenge, making dependability a fundamental requirement. To address these challenges, various fault-tolerance techniques have been developed to improve system availability and resilience, enabling service continuity even in the case of failure events. Formal methods provide mathematically rigorous techniques for modeling, analyzing, and verifying the dependability of cellular systems. This paper presents a comprehensive survey of formal method applications in dependability analysis for cellular access networks, classifying existing approaches by network generation, modeling framework, and fault-tolerance strategy. Finally, we highlight several open security-related issues that remain open in current cellular access networks, and that guide our ongoing research.

Graph processing frameworks are pivotal in managing the increasing complexity and size of datasets in numerous computational fields. However, the performance of these frameworks can vary significantly depending on their design and the specific conditions under which they are tested. This paper presents a comprehensive benchmarking study of six single-machine graph processing frameworks: GraphChi, Ligra, X-stream, MMap, GridGraph, and GPOP across a variety of datasets and graph processing algorithms, and on a consumer-level machine. In the evaluation of the frameworks, several performance metrics were used, which are execution time, CPU, and memory usage, as well as qualitative metrics, such as ease of use and comprehensive documentation which contribute to determining each framework’s practical effectiveness. Our findings indicate that no single framework excels in all aspects; instead, each framework demonstrates strengths and weaknesses that are context-dependent. By evaluating frameworks in a unified environment rather than their original setups, the study explores which frameworks perform more effectively under comparable conditions.

Data privacy and security is becoming one of the most important subjects for IT companies, as it has the potential to shift their reputation and therefore influence their value on the market. However, on a large scale, namely in Big Data platforms, securing data may be a major challenge as it can limit the system's performance. Therefore, finding solutions that enable a compromise between security and performance is a must. In this article, we present a framework called Distributed Cipher Chaining (DCC) which allows the creation of flexible encryption schemes that can offer configurable levels of availability. We also present a local multi-threaded implementation as well as a distributed multi-process implementation and the advantages and applications of each one. We show that our solution is well adapted to large files as it outperforms state-of-the art methods while improving the diffusion rate.

Two important Quality-of-Service (QoS) measures for cellular networks are the fractions of New Calls (NCs) and Handoff Calls (HCs). These types of calls are usually blocked or dropped for two reasons: radio channels are occupied (performance reason) or failure of radio channels (availability reason). Call Admission Control (CAC) is a technique that accepts or rejects user requests in a network. This paper proposes two new CAC schemes for Long Term Evolution (LTE) networks supporting two classes of services (Real-Time (RT) and Non-Real-Time (NRT)). The proposed CAC schemes are composites, meaning that they consider performance changes associated with the failure and recovery of radio channels. We use the Probabilistic Model Checking (PMC) to perform a comparative analysis between the performability measures (combination of performance and availability measures) of the proposed composite CAC schemes and an existing pure performance model. First, we model the composite CAC schemes with multidimensional Continuous Time Markov Chain (CTMC). Then, we specify QoS requirements through the CTMC using the Continuous-time Stochastic Logic (CSL). Finally, we quantify the performability measures of the composite CAC schemes by checking CSL steady-state, transient, and path formulas using the PRISM model checker.

Graphs are increasingly adopted to model and handle complex systems, but their processing is known to be resource-intensive due to the complexity of the algorithms and the size of the graphs. This hindrance limits their usage for those who do not possess sophisticated equipment with “unlimited” memory space. In this paper, a new graph format called compressed edge-centric (CEC) is proposed, aiming to reduce memory usage by compressing graph edges, facilitating more efficient large graph handling. It is then followed up by the implementation of several graph creation approaches, each using a different graph representation and parallelism level. The idea is to use a predictive model to estimate the execution time and used memory, along with a decision-making process that will automatically choose the best approach by selecting the lowest predicted time that does not overload the memory for a given graph and in a certain hardware environment. Experiments on diverse real-world graphs, sourced from the Network Repository, demonstrate that CEC-based creation methods are more efficient than vertex-centric techniques in terms of time (up to 60% decrease) and in many cases in terms of memory consumption (up to 50% decrease). Since this efficiency is not uniformly observed, this work relies on machine learning models to predict the time and memory of each approach for a given context. The results show that linear models are not adequate to thoroughly predict time and memory consumption, while tree-based solutions give considerably better results.

Cloud Radio Access Network (C-RAN) has been proposed as a cloud architecture to provide a common connected resource pool management. It separates the functionalities of the traditional Base Station (BS) into two parts: the Base Band Unit (BBU) and the Remote Radio Head (RRH). BBUs functions are implemented on the Virtual Machines (VMs) in the cloud over commodity hardware, serving User Equipments (UEs) by generating VMs. In this regard, a more accurate adjustment of the number of VMs in a BBU is a challenge. This paper proposes a VM allocation scheme in C-RAN using the hysteresis and migration mechanisms jointly. The goal is to ensure the system’s load balancing and preserve energy. The hysteresis mechanism with different thresholds adjusts the number of active VMs required to serve all UEs by putting idle VMs in sleep mode and activating them as needed. Whereas, the load balancing is achieved by the proposed allocation scheme and the migration of calls from most loaded to least loaded BBU. We use Discrete-Time Markov Decision Processes (MDPs) to enhance both the performance and energy efficiency in the VM allocation schemes. These objectives are achieved by the different decisions of a controller, who should choose the best decision at each time slot. We analyze the performance of the proposed scheme by Probabilistic Model Checking (PMC). Performance requirements are specified using Probabilistic Computation Tree Logic (PCTL) suitable for MDP models. We also check multi-objective properties, by generating Pareto curves, to evaluate the tradeoff based on which the controller can decide. We use the PRISM model checker to build and analyze the MDP models.

PDDL is a de facto standard language for formally describing planning problems. It is equipped with dynamic tools for executing PDDL descriptions. But, it is not equipped with static tools allowing to reason a priori on the correction of the PDDL descriptions. To remedy this shortcoming, we have designed, produced and tested a tool called PDDL2EventB in order to automate the approach and the systematic translation rules from PDDL to Event-B. This allows a formal static verification of PDDL descriptions and exploit the static tools associated with Event-B. To achieve this, we successfully used the Xtext MDE tool creating an integrated development environment specific to the PDDL language, and the Xtend tool to implement our transformation and produce the Event-B models according to a top-down approach.

Call Admission Control (CAC) plays a significant role in providing the desired Quality of Service (QoS) in mobile-cellular networks. This paper extends from a previous work in which we proposed a performance evaluation of CAC schemes in mobile cellular networks supporting two classes of services Real-Time (RT) and Non-Real-Time (NRT). The performance of CAC schemes is traditionally evaluated by computing the following steady-state measures: the new call blocking probability, the handoff call dropping probability, and the mean channels occupation rate. We present, in this paper, a detailed comparative evaluation of different CAC schemes proposed in a previous work using formal methods. Furthermore, we propose quantifying more relevant performance measures using the probabilistic model checking. Indeed, we evaluate the performances of the investigated schemes by computing not only the traditional performance measures, but also transient and path-based performance measures. These measures are specified using the branching-time logic Continuous-time Stochastic Logic (CSL). With CSL, we can express QoS requirements over a selective set of paths through the formal model of the considered CAC schema, which is modeled by Continuous-Time Markov chains (CTMCs). We quantify performance measures by checking CSL formulas using the PRISM model checker.

We present in this paper Phi, a generic microservices-based Big Data architecture dedicated to complex multi-layered systems, that rallies multiple machine learning jobs, stream and batch processing. We show how to apply our architecture to an adaptive e-learning application that adjusts its recommendation to the emotions of the learner on the spot. We deploy our application on the cloud using AWS services, and perform some performance tests to show its feasibility in a realistic environment.

For the fifth-generation (5G), Cloud Radio Access Network (C-RAN) has been proposed as a cloud architecture to provide a common connected resource pool management. In this regard, considering the rapidly changing in network traffic load, the efficient management of radio resources is a challenge. Call Admission Control (CAC) is a resource allocation mechanism to guarantee the Quality of Service (QoS) to User Equipment (UE) in a mobile cellular network. This paper proposes a new CAC schema, based on a hysteresis mechanism, named Virtual Machine Hysteresis Allocation Strategy (VMHAS) in the context of C-RAN. We aim to provide a good QoS by improving the blocking probability of calls, adjusting the amount of active VMs being provisioned for the current traffic load, and providing a load balancing in the considered C-RAN. We use probabilistic model checking to evaluate the performance of the proposed strategy. First, we model the VMHAS CAC schema with Continuous-Time Markov Chains (CTMCs). Then, we specify QoS requirements through the CTMC using the Continuous-time Stochastic Logic (CSL). Finally, we quantify the performance measures of the considered strategy by checking CSL steady-state and transient formulas using the PRISM model checker.

The formal Event-B method makes it possible to obtain systems or software correct by construction. The modeling activity aims to establish formal models in Event-B. As for the proof activity, it aims at correcting these models. A proven Event-B model is not necessarily valid. We propose to open the Event-B formal method on PDDL in order to further validate Event-B models. We aim to validate the dynamic properties related to the sequence of events authorized on Event-B models. PDDL is a de facto standard language for planning problems. It is equipped with planners to automatically generate solution-plans. To achieve this, we successfully used the MDE approach, Xtext to create an integrated development environment specific to the Event-B language and the Xtend tool to implement our transformation EventB2PDDL and produce PDDL descriptions using a top-down approach.

SummaryOne of the most critical properties that must be ensured to have a secure electronic voting is verifiability. Political parties, observers, and especially voters want to be able to verify that all eligible votes are cast as intended and counted as cast without compromising votes secrecy or voters privacy. Over the past few decades, an important number of e‐voting protocols attempt to deal with this issue by using cryptographic techniques and/or a public bulletin board. Recently, some blockchain‐based e‐voting systems have been proposed, but were not found practical in the real world, because they do not support situations with large numbers of candidates and voters. In this article, we design and implement a verifiable blockchain‐based online voting protocol, called verify‐your‐vote . Our protocol ensures several security properties thanks to some cryptographic primitives and blockchain technology. We also evaluate its performance in terms of time, cost, and the number of voters and candidates that can be supported.

Big Data systems are now present in almost all mature organizations and not just IT focused ones. From luxury hotels to health care organizations, data storage and processing is witnessing a huge technological improvement thanks to the extensive research that is being conducted to improve these two areas. However, there is a lack of adaptability when it comes to security and more importantly encryption, as traditional security solutions are still being used today without any changes that can adapt them to Big Data environments. In this article, we are interested in working on data at rest encryption in a big data environment. In particular we pay special attention to distributed storing as well as large volumes of data. We base our work of a very known encryption mode of operation called CBC which is heavily used for data at rest encryption, but suffers from the high cost of running sequential encryption over the entire plaintext. Our solution offers an alternative that guarantees the same properties as CBC, and even enhances some of them (namely the diffusion property), while offering the possibility for parallel encryption which makes it more efficient especially in distributed environments. These claims will be proved using a set of theoretical equations that will be detailed in the article.

Hybrid Cloud environments allow the utilization of local resources in private Clouds with resources from public Clouds when needed. Such environments represent systems with high failure rates because they feature heterogeneous components, a large number of servers with intensive workload are built as complex architectures. For these reasons, the availability of such systems could be easily compromised if the failure of these heterogeneous components is not handled correctly, which may cause request rejection and frequent performance degradation. Providing highly reliable Cloud applications, in particular in a hybrid Cloud environment, is a challenging and critical research problem. Therefore, the question we address in this paper is how to provision resources to user requests in the presence of failures in a hybrid Cloud environment. To this end, we propose a reconfigurable formal model of the hybrid Cloud architecture, then we utilize instantiations of this model, simulation and real-time execution runs to estimate different performance metrics related to fault detection and self-recovery strategies in hybrid Cloud. Our approach is based on the combination of the model-based and the probabilistic approaches. Hybrid Cloud environments allow the utilization of local resources in private Clouds with resources from public Clouds when needed. Such environments represent systems with high failure rates because they feature heterogeneous components, a large number of servers with intensive workload are built as complex architectures. For these reasons, the availability of such systems could be easily compromised if the failure of these heterogeneous components is not handled correctly, which may cause request rejection and frequent performance degradation. Providing highly reliable Cloud applications, in particular in a hybrid Cloud environment, is a challenging and critical research problem. Therefore, the question we address in this paper is how to provision resources to user requests in the presence of failures in a hybrid Cloud environment. To this end, we propose a reconfigurable formal model of the hybrid Cloud architecture, then we utilize instantiations of this model, simulation and real-time execution runs to estimate different performance metrics related to fault detection and self-recovery strategies in hybrid Cloud. Our approach is based on the combination of the model-based and the probabilistic approaches.

Quality of web service becomes more and more interesting as a distinguishing criterion to select a unique web service from all candidate ones. The quality assessment issue, especially regarding the volatility of the web services environment, is one among the main challenges in this context. In this paper, we propose a service-based system for web services monitoring. Compared with other efforts in this concern, our proposal is closer to the client's non-functional requirements, more accurate and extensible to support new quality attributes.

Information is one of the most important factors in business success, hence the importance of the Business Intelligence (BI) domain in order to simplify the decision making and make it more relevant. Decisional systems have been used for several years to help decision-makers access, analyze and extract value from the data that their organisation accumulated through the years. The success gained by these types of systems caused the establishment of a well-known architecture and development chain, and the proliferation of tools and methodologies that have proven their value. Nonetheless, in some use cases, the classical decisional architecture shows some shortcomings. In fact, the traditional storage and processing models in Business Intelligence systems are not sufficient anymore when confronted with data that becomes more and more massive, varied and with a high velocity. This is where Big Data solutions can be of great use. In fact, these solutions have proven their efficiency when dealing with enormous constantly increasing amounts of data with a changing schema. Our goal in this article is to show the various manners to integrate big data solutions into the decisional world, and to help architects choose which architecture corresponds better to their needs, by taking into consideration the environmental, technical and functional constraints they are faced with.

Since the rise of Big Data, working with large files became the rule and no longer the exception. Despite this fact, some data at-rest encryption modes of operation, namely CBC, are being used even though they do not take into account the heavy cost of running sequential encryption operations over a big volume of data. This led to some attempts that aim to parallelizing such operations either by only chaining isolated subsets of the plaintext, or by using hash functions to reflect any changes made to the plaintext before running parallel encryption operations. However, we noticed that such solutions present some security issues of different levels of severity. In this paper, we propose a Distributed version of CBC, which we refer to as DCBC, that uses an IV generation layer to ensure some level of chaining between multiple CBC encryption operations that run in parallel, while keeping CPA security intact and even adding new operations such as appending data without compromising the encryption mode's security. We will, also, make a theoretical performance comparison between DCBC and CBC under different circumstances to study optimal conditions for running our proposed mode. We show in this comparison that our solution largely outperforms CBC, when it comes to large files.

Big Data technologies and approaches have an important impact on the organization and governance of the enterprise. With such a high volume of structured & unstructured data, real time and mutualization needs, it is quite complicated to keep a high quality of data by respecting the governance rules and best practices. In addition, new team roles and organization must be applied in order to adapt to the new Big Data decisional constraints. In this direction, we present in this paper an overview of DECIDE, a decisional Big Data Methodology. We focus, particularly, on its team workforce, data quality, storage and governance fundamentals, rules and steps.

With the immutability property and decentralized architecture, Blockchain technology is considered as a revolution for several topics. For electronic voting, it can be used to ensure voter privacy, the integrity of votes, and the verifiability of vote results. More precisely permissioned Blockchains could be the solution for many of the e-voting issues. In this paper, we start by evaluating some of the existing Blockchain-based e-voting systems and analyze their drawbacks. We then propose a fully-decentralized e-voting system based on permissioned Blockchain. Called DABSTERS, our protocol uses a blinded signature consensus algorithm to preserve voters privacy. This ensures several security properties and aims at achieving a balance between voter privacy and election transparency. Furthermore, we formally prove the security of our protocol by using the automated verification tool, ProVerif, with the Applied Pi-Calculus modeling language.