Microservices auto-scaling is an attracking research domain focusing on the dynamic definition of strategies to optimize system efficiency and performance while minimizing service cost. An efficient auto-scaling strikes a balance between individual microservices quality requirements while collaborating to uphold the overall system quality. Maintaining such balance needs a formal method to establish relevant parameters to ensure quality attributes and enable prior accuracy and efficiency verification. To that end, we extend the Petri net model to define Hierarchical Parallel Petri nets (HPPNs) to correctly model both autonomy and cooperation of microservices. Unlike conventional Petri nets, HPPNs consider trade-offs between tokens during transitions, enabling the computation of compromises between multiple quality dimensions and the adaptation strategies. Additionally, preliminary testing mechanisms define the qualities of individual components, providing a solid foundation for assessing microservices’ performance and quality attributes.

microservices are subject to an unpredictable and variant workload that challenges their quality of service. There-fore, several approaches emerge in the literature proposing auto-scaling policies as a promising solution to deal with such unpredictable increase/decrease of the workload. However, they generally deal with a specific and unique quality of service as cost-aware, latency-aware and other specific quality-awareness. We propose a multicriteria approach for microservice-based applications' auto-scaling. By means of a layered architecture, we present a hybrid auto-scaling solution that ensures an autonomous auto-scaling of microservices to enable them maintaining their specific required qualities. Moreover, a cooperative policy is applied to maintain the system overall qualities by identifying a compromise plan when the adaptation concerns different qualities of the system. The present work combines the efficiency of the hybrid strategy with the multicriteria selection principle to reach an autonomous-cooperative auto-scaling approach.

Emergency is an essential mission of public hospitals, one of its main features is to meet requirements expected by the population, whatever their nature. This work proposes a fog-based architecture integrating intelligent algorithms; based on machine learning models, to improve the emergency department performance and the patient experience. The proposed architecture effectiveness is ensured via the fog infrastructure where interactions between the smart scheduling system; deployed on the cloud, and the doctors are maintained. To ensure the efficiency property, we adopt machine learning algorithms to assign and classify patients with regards to the urgency of their cases, their waiting time and physician's availability.

Self-adaptive systems (SAS) have the ability to achieve functional and/or quality of service objectives by automatically modifying their behavior at runtime. Accordingly, each self-adaptive system typically consists of a managed system dealing with the domain concerns, and a feedback loop handling adaptation concerns of the managed system. In the aim to promote the actual use of these systems, it is necessary to cope with underlying uncertainty and variability of their execution environments. However, existing approaches lack formal models and/or tools to engineer all aspects of self-adaptation. In this paper, we propose a formal approach for modeling, developing and analyzing quality-aware SASs under uncertainty. We mainly focus on non-deterministic selection of adaptation plans. The approach is based on probabilistic rewrite theories to address adaptation planning. The formal model is defined using PSMAUDE which allows specifying nonfunctional requirements, strategies and probabilistic systems features.

Many approaches on context-aware systems specification have been proposed in the literature. However, the absence or poor representation of contextual information and its relationships with system entities in these approaches usually leads to low-precision and irrelevant results. The aim of this paper is to promote the ability to specify and verify context-aware systems. Our proposed modeling methodology exploits Maude reflection and meta-programming to define a domain specific language for context-aware systems specification and adopts Maude model checker to verify system inherent properties. Moreover, a runtime environment implementing the proposed model is developed for pervasive context-aware systems execution.

Cloud computing is an emerging topic in the IT industry, it brings new design challenges and security issues, as resources rapid availability and quick scalability. Since formal methods provide a reliable mathematical basis giving rise to safely analyzable models, we aim in this paper to propose a formal framework for cloud computing architectural elasticity. Bigraphical Reactive Systems are adopted as a semantic framework for their graphical aspect and rigorous basis. Then, Maude language is used to implement the obtained cloud bigraphical model. Maude system allows us to execute and analyze the formal specification of cloud computing architecture and its elasticity.

Petri nets have been used as a formal semantic framework for UML activity diagrams. With UML 2.0 extensions, they become not able to express high level constructions in activity diagrams, namely the traverse-to-completion concept. This one requires a global synchronization between the fork and join nodes which is totally absent in ordinary Petri nets, based on local synchronization. To conserve activities behaviors, we propose zero-safe nets as a richer and more adapted semantic framework for activity diagrams by giving a generic mapping from activities to this Petri nets class. The proposed mapping preserves activities operational semantics while focusing on traverse-to-completion principle as well as synchronization between fork and join nodes and therefore, covering control/data flows and concurrency.

Due to the proliferation of Internet and wireless communication networks, mobility of software components is pervasive in current applications. However, most of the existing Architecture Description Languages (ADLS) lack operators to express mobility primitives. In this paper, we propose a generic rewrite theory for mobility in CBabel, a Declarative Architecture Description Language. Rademaker et al. have associated a rewriting logic semantics to the different constructors of CBabel. We exploit such semantics to extend CBabel with mobility primitives by defining a rewrite theory called mobility-primitives. Our objective is two folds: We propose a rewrite theory for mobility in CBabel. Then, we generalize it to any Architecture Description Language that can be translated to rewriting logic. Such generalization will be obtained by introducing the parameterization notion of Full Maude to the mobility-primitives rewrite theory.

An architectural model for distributed systems description, based on tile logic, has been proposed in a previous work. It is based on dynamic connections between components. A distributed system, in this model, is defined as a set of individual components that are completely free from static interconnection constraints and a dynamic connection is created only if an interaction between two components is needed. Our aim in this paper is to show how a space dimension can be easily added to our architectural model in order to support mobile applications description. A conference reviewing case study is presented to illustrate the benefits of our architectural model.