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

De Ensiwiki
Révision de 24 avril 2015 à 08:22 par Delanaur (discussion | contributions) (Réflexion sur des problèmes ouverts)

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 répartis peuvent être modélisés et fonctionnent comme des systèmes communicants, c'est à dire par des messages qui transitent via 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 Web Client/Serveur : le client va envoyer un message au serveur, et en attendre sa réponse. Mais aussi par exemple le fonctionnement d'une gare, d'un système de réservation de billets, ou même d'un distributeur de boissons... Dans tous les cas, on peut formaliser ce système communicant par des systèmes de transitions labellisés (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 nœuds, et les transitions représentent les échanges de messages (avec un symbolisme différent selon la nature du message : par convention, le nom du message est par exemple suivi d'un "!" si il s'agit d'une envoi, et d'un "?" s'il s'agit d'une réception).


Exemple de système modélisé par des LTS
Exemple de système modélisé par des LTS

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, puisque si le système est synchro

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.

Résultats à exploiter

Analyse de problèmes ouverts

Analyse structurelles de systèmes

Calcul des bornes de buffers

Performances

Uniformité des bornes

Réflexions théoriques et formelles

Comprendre le problème

Dépendances de cycles

Limites de l'approche

Réalisations et résultats

Reprise du code existant

Algorithmes et tests

Observations

Futurs travaux ?