Arléon Zemtsop joins Spirals

sbliudze

Arléon Zemtsop has joined Spirals on the 1st of October as a Software Engineer working on the ANR SmartCloud project.

The SmartCloud project, among its broader objectives, aims to develop a coordination prototype based on behavioral models of Cloud Computing (CC) systems. These models will explicitly represent operational modes and resource usage with two primary goals: ensuring system safety through a control infrastructure and facilitating efficient resource utilization via monitoring and optimization.

To support these objectives, we are defining a new formalism for organizing architectural, behavioral, and quantitative information on CC systems, including hosted applications. This formalism follows the “MAPE-K” (Monitor-Analyze-Plan-Execute with Knowledge base) approach, enabling CC systems to adapt dynamically to environmental changes. Arléon will contribute to the design of a prototype tool that implements this formalism using JavaBIP.

This work is part of SmartCloud’s overarching mission to enhance the resilience, safety, and efficiency of Cloud infrastructures through a coordinated, model-based adaptation framework.

Design of correct-by-construction self-adaptive cloud applications using formal methods

sbliudze

Essentially, any software entity that goes beyond simply computing a certain function necessarily has to interact and share resources with other such entities. Correct coordination of access to resources among concurrent software entities is fundamental to ensuring that they satisfy user and system requirements avoiding operational faults and deadlock situations. This proposal targets the correct coordination of access to cloud resources among concurrent cloud application entities.

Trinh Le Khanh

Trình Lê Khánh has defended his PhD on the 27th of January, 2023. Congratulations Trình!

Read more →

Feature Models vs BDD size: Impact analysis

sbliudze
PDF of the proposal

We work on an approach that leverages feature models for acquiring a compact representation of a set of valid configurations of a system in the form of a JavaBIP model used to control the software system at run time. The goal of this project is to propose and evaluate new approaches to the analysis of the impact of the feature model shape on the size of the Binary Decision Diagrams (BDDs) that encode it in JavaBIP (and thereby on the ensuing JavaBIP engine overhead).

Read more →

Aggregate measures for control and coordination of IoT systems

sbliudze
PDF of the proposal

The main goal of this project is to propose specification mechanisms for the coordination and control based on aggregate measures, such as the percentage of entities in a given state, e.g. if less than 75% of system blocks have enough charge to emit light for 5 minutes, then 20% of these blocks shall switch off their speakers (thus allowing these blocks to continue emitting light for a longer period).

Read more →

Self-adaptive modular robots: formal modeling for validation and coordination

sbliudze

The main objective of this project is to contribute to the implementation of modular robots by developing a formal framework to model, validate and coordinate their dynamic behaviours. The scientific challenges consist in particular in the ability to model the dynamic evolution of this type of complex systems—their adaptation and reconfiguration—by taking into account constraints on resources as well as events occurring in their execution environment.

This project is submitted for joint funding with the French Agency for Defence Innovation (AID). Therefore, we are currently looking only for candidates holding EU, United Kingdom or Swiss citizenship.

Read more →