Séminaires

This talk presents research contributions on Boolean Satisfiability (SAT) solving and its application to the analysis of discrete systems. The first part focuses on parallel SAT solving, addressing key issues such as modular solver design, the articulation between divide-and-conquer and portfolio approaches, and effective learned-clause sharing. In this context, the PaInleSS framework is introduced as a generic platform for building efficient parallel SAT solvers. The second part considers domain-aware SAT solving through programmatic extensions of CDCL, showing how problem-specific knowledge can improve solving strategies, especially in bounded model checking. The presentation concludes with an application to the verification of blockchain smart contracts, where SAT-based reasoning provides a promising basis for analyzing security- and safety-critical properties at scale.

Ce séminaire présente des travaux portant sur le développement d’approches formelles centralisées, modulaires et distribuées pour la modélisation, le contrôle, l’analyse des performances, la reconfiguration et la cybersécurité des systèmes à événements discrets. Ces travaux s’appuient sur différents formalismes tels que les réseaux de Petri (temporisés et colorés), les automates temporisés avec gardes, les automates hybrides, ainsi que les algèbres Max-Plus et Min-Plus et les séries formelles colorées. L’objectif est de proposer des méthodes d’analyse et d’aide à la décision permettant de garantir certaines propriétés des systèmes, notamment en termes de performance, de sûreté et de résilience. Une attention particulière est portée aux problématiques de modélisation et de vérification analytique dans des architectures d’automatisation distribuées (collaboration avec EDF). Les techniques formelles établies sont illustrées à travers plusieurs domaines d’application, notamment la résilience des chaînes logistiques, l’analyse du temps de réponse des systèmes de commande en réseau, les systèmes manufacturiers soumis à contraintes et la sécurité des systèmes cyber-physiques.

Les applications IoT déployées dans le continuum IoT–Fog–Cloud doivent concilier des contraintes de ressources, qualité de service (QoS), hétérogénéité et dynamique d’exécution, tout en restant robustes face aux pannes. Dans ce contexte, la fiabilité ne peut pas reposer uniquement sur des tests ad hoc : elle doit être construite et argumentée de manière systématique, depuis les exigences jusqu’au comportement observé en exécution. Nous présentons d’abord une approche centrée sur la vérification de mécanismes de tolérance aux pannes dans l’IoT multi-couches. La modélisation en Event-B, via raffinement et invariants, permet de formaliser des stratégies telles que la dégradation contrôlée, le basculement vers des composants de secours et la reprise/retour à un état sûr, tout en générant des obligations de preuve garantissant que ces mécanismes préservent les propriétés de sûreté attendues. Cette étape pose un socle : la résilience doit être spécifiée et justifiée rigoureusement, couche par couche, dans des architectures distribuées. Nous passons ensuite au Fog, où l’enjeu devient la composition de services sous contraintes, depuis les exigences jusqu’au déploiement (et, le cas échéant, l’interaction avec des services cloud). La démarche se décline en étapes : (i) capturer et structurer les exigences (fonctionnelles, coordination, ressources, QoS), (ii) décider un placement correct des composants, (iii) établir une configuration/reconfiguration d’un service composite en arbitrant entre efficacité QoS et fiabilité (notamment transactionnelle), puis (iv) vérifier formellement la cohérence de la composition et des interactions par Event-B. Dans cette dynamique, une perspective consiste à mobiliser des agents conversationnels (systèmes multi-agents conversationnels) pour soutenir l’orchestration et la reconfiguration (négociation de contraintes, adaptation, selection, assistance à la décision), tout en conservant un noyau formel vérifiable. Enfin, nous motivons une évolution méthodologique : Event-B est très puissant pour prouver des invariants et structurer la correction, mais il n’est pas toujours le plus adapté pour explorer exhaustivement certains comportements dynamiques typiques des systèmes distribués (interleavings concurrents, scénarios d’exécution, blocages, vivacité, effets de reconfiguration). Pour couvrir ces aspects, nous proposons de compléter la preuve par du model checking, en introduisant une transformation Event-B ? Réseaux de Petri Colorés (CPN). Cette transformation vise à obtenir un modèle exécutable et analysable, permettant ensuite d’appliquer des techniques de vérification automatique (exploration d’espace d’états, détection de deadlocks, propriétés de vivacité/atteignabilité) et de refermer la boucle : les contre-exemples et scénarios trouvés alimentent l’amélioration du modèle Event-B, des exigences et des politiques de configuration. Mots-clés Continuum IoT–Fog–Cloud, Fiabilité / Résilience, Qualité de service (QoS), Tolérance aux pannes multi-couches, Composition et (re)configuration de services, Placement sous contraintes, Vérification formelle, Event-B, Réseaux de Petri colorés (CPN), Model checking, systèmes multi-agents conversationnels

Rational synthesis studies the automatic construction of controllers that interact with rational agents pursuing their own objectives. Rather than assuming a hostile environment, this framework accounts for strategic behavior and equilibrium reasoning in multi-agent systems. In this talk, we consider rational synthesis in the presence of shared resources. Agents interact in turn-based games where actions may consume or replenish common resources, and must satisfy qualitative temporal objectives while avoiding resource depletion. We discuss how resource constraints fundamentally impact the synthesis problem, how the model evolves from single to multiple resources, and what this reveals about the limits of automated controller design.

This talk is organized into three main parts. The first part introduces research on Petri net structure theory and robust/adaptive supervisory control of discrete event systems, including controllability of siphons, supervisory control based on time constraints, and robust/adaptive supervisory control for systems with uncertainties caused by unreliable resources or operations. The second part concerns security analysis and resilient control of cyber-physical systems (CPSs) under information impairment. It discusses opacity analysis and resilient supervisory control strategies in the presence of cyberattacks and malicious intrusions. Furthermore, the talk addresses fault diagnosis in CPSs with communication delays. Finally, the talk highlights several future research directions, including prognosability analysis in CPSs with communication delays and the integration of data-driven approaches with supervisory control theory, aiming to enhance the security and resilience of next-generation CPSs.