Remy Delanaux (avec Gwen Salaun) : Stabilité des systèmes communicants

De Ensiwiki
Aller à : navigation, rechercher
Cornues.png
Titre du projet Stabilité des systèmes communicants
Cadre IRL

Labo INRIA, LIG
Équipe CONVECS
Encadrants Gwen SALAÜN et Lakhdar AKROUN


Introduction

Présentation du sujet

Les systèmes communicants

De très nombreux systèmes et programmes informatiques peuvent être modélisés et fonctionnent comme des systèmes communicants, c'est à dire par des messages par des canaux de communication, en particulier par une succession d'envois et de réceptions de ces messages. On peut citer par exemple des architectures Client/Serveur, le fonctionnement d'une gare, d'un système de réservation de billets, ou même d'un distributeur de boisson par exemple... Dans tous les cas, on peut formaliser ce système communicant par des automates (abrégé en LTS, pour Labeled Transition System), représentant chacun une brique fonctionnelle du système, et où les différents états du système servent de sommets, et les transitions représentent les échanges de messages (avec un symbolisme différent selon la nature du message : traditionnellement, le nom du message est par exemple suivi d'un "!" si il s'agit d'une réception, et d'un "?" s'il s'agit d'un envoi).

Systèmes asynchrones : entre buffers et stabilité

Les systèmes communicants peuvent fonctionner de façon synchrone (imaginez une discussion au téléphone : les 2 interlocuteurs sont au téléphone en même temps, l'appelant doit attendre une réponse de l'appelé pour réaliser l'appel) ou asynchrone (un échange de mail par exemple ; les envois et réceptions peuvent être détachés dans le temps). Dans notre cas, tous les systèmes sont considérés asynchrones au départ, et certaines vérifications formelles permettent de vérifier sa synchronisabilité : le cas échéant, le traitement en est simple.

Dans le cas contraire, il faut bien pouvoir conserver les messages envoyés mais pas encore reçus par le destinataire : cela se fait dans des buffers, modélisés par une FIFO. Si le système est cyclique, il peut y avoir besoin de buffers infinis, donc d'un espace d'états infini pour représenter tous les états possibles du système. Pire encore : savoir si un système se comporte "correctement" (pas d'interblocage, par exemple) est indécidable [JACM83].

On peut toutefois utiliser des techniques de vérification formelles utilisées pour les systèmes finis, en cherchant des sous-classes de systèmes infinis analysables, car possédant d'autres propriétés.


Contexte de recherche

Réflexions théoriques et formelles

Sur quoi influer ?

Heuristiques

Dépendances de cycles

Implémentation et résultats

Algorithmes utilisés

Observations

Futurs travaux ?