A formal framework for the specification and verification of distributed processes communication flows in clouds
Clouds are constituted of servers interconnected via the Internet, on which systems can be implemented, making use of applications and databases deployed on the servers. Cloud-based computing is gaining in popularity, and that includes the context of critical systems. As a result, it is useful to define formal frameworks for reasoning about cloud-based systems. One requirement about such a framework is that it enables reasoning about the concepts manipulated in a cloud, which naturally includes the ability to reason about distributed systems, composed of subsystems deployed on different machines and interacting through message passing to implement services. In this context, the ability to reason about communication flows is central. The aim of this thesis is to define a formal framework dedicated to the specification and verification of systems deployed on clouds. This framework will capitalize on the formal framework of "interactions". Interactions are models dedicated to the specification of communication flows between different actors in a system. The thesis work will study how to define structuring (enrichment, composition) and refinement operators to enable the implementation of classical software engineering processes based on interactions.
Analysis and design of dispersion-engineered impedance surfaces
Dispersion engineering (DE) refers to the control of how electromagnetic waves propagate in a structure by shaping the relationship between frequency and phase velocity. Using artificially engineered materials and surfaces, this relationship can be tailored to achieve non-conventional propagation behaviors, enabling precise control of dispersive effects in the system. In antenna design, dispersion engineering can enhance several key aspects of radiation performance, including gain bandwidth, beam-scanning accuracy, and in general the reduction of distortions that arise when the operating frequency changes. It can also enable additional functionalities, such as multiband operation or multifocal behavior in lens- and reflector-based antennas.
This thesis aims to investigate the underlying physics governing the control of phase and group velocities in two-dimensional artificial surfaces with frequency-dependent effective impedance properties. A particular emphasis will be placed on spatially fed architectures, such as transmitarrays and reflectarrays, where dispersion plays a crucial role. The objective is to derive analytical formulations within simultaneously control of both group and phase delay, develop general models, and assess the fundamental limitations of such systems in radiation performance. This work is especially relevant for high-gain antenna architectures, where the state of the art remains limited. Current dispersion-engineered designs are mostly narrowband, and no compact high-gain solution (> 35 dBi) has yet overcome dispersion-induced degradations, which lead to gain drop and beam squint.
The student will develop theoretical and numerical tools, investigate new concepts of periodic unit cells for the impedance surfaces, and design advanced antenna architectures exploiting principles such as true-time delay, shared-aperture multiband operation, or near-field focsuing with minimized chromatic aberrations. The project will also explore alternative fabrication technologies to surpass the constraints of standard PCB processes and unlock new dispersion capabilities.
AI-Driven Network Management with Large Language Models LLMs
The increasing complexity of heterogeneous networks (satellite, 5G, IoT, TSN) requires an evolution in network management. Intent-Based Networking (IBN), while advanced, still faces challenges in unambiguously translating high-level intentions into technical configurations. This work proposes to overcome this limitation by leveraging Large Language Models (LLMs) as a cognitive interface for complete and reliable automation.
This thesis aims to design and develop an IBN-LLM framework to create the cognitive brain of a closed control loop on the top of an SDN architecture. The work will focus on three major challenges: 1) developing a reliable semantic translator from natural language to network configurations; 2) designing a deterministic Verification Engine (via simulations or digital twins) to prevent LLM "hallucinations"; and 3) integrating real-time analysis capabilities (RAG) for Root Cause Analysis (RCA) and the proactive generation of optimization intents.
We anticipate the design of an IBN-LLM architecture integrated with SDN controllers, along with methodologies for the formal verification of configurations. The core contribution will be the creation of an LLM-based model capable of performing RCA and generating optimization intents in real-time. The validation of the approach will be ensured by a functional prototype (PoC), whose experimental evaluation will allow for the precise measurement of performance in terms of accuracy, latency, and resilience.