MEXICO (SR0358LR)
Modeling and Exploitation of Interaction and Concurrency
MEXICO
→
MEXICO (SR0468FR)
Statut:
Terminée
Responsable :
Stefan Haar
Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" :
Aucun mot-clé.
Mots-clés de "B - Autres sciences et domaines d'application - 2023" :
Aucun mot-clé.
Domaine :
Algorithmique, programmation, logiciels et architectures
Thème :
Programmation, vérification et preuves
Période :
01/03/2009 ->
31/12/2010
Dates d'évaluation :
Etablissement(s) de rattachement :
<sans>
Laboratoire(s) partenaire(s) :
<sans UMR>
CRI :
Centre Inria de Saclay
Localisation :
ENS Cachan - Laboratoire Spécification et Vérification (LSV)
Code structure Inria :
Numéro RNSR :
200920937Y
N° de structure Inria:
SR0358LR
Présentation
Dans un environnement où les réseaux sont de plus en plus présents, la
fiabilité des applications devient d'autant plus critique que le nombre
d'utilisateurs des systèmes de communication, services Web, moyens de
transport, etc., augmente constamment. Les travaux de MExICo ont pour
motivation une meilleure compréhension et une fiabilité accrue des
systèmes distribués asynchrones, et s'intéressent particulièrement à la
concurrence et à l'interaction. Avec la taille croissante et le
déploiement en réseau des systèmes de communication, des contrôleurs, des
services etc. nous sommes confrontés à un très grand degré de parallélisme
entre les processus locaux. Dans toutes les formes d'analyse et de
contrôle, une vision globale du système conduit à une explosion du nombre
d'états et de transitions, qui nuit à la mise en valeur des mécanismes mis
en œuvre. À l'inverse, en respectant la concurrence, on évite
l'énumération exhaustive des entrelacements, et on peut se concentrer sur
les propriétés essentielles des comportements non séquentiels caractérisés
par les relations de causalité. Nous voyons la concurrence dans les
systèmes distribués comme une opportunité plutôt qu'un obstacle qui
conduit à l'explosion du nombre d'états des modèles formels et ralentit
les algorithmes.
Axes de recherche
-
Diagnostic et diagnosticabilité. Le problème du diagnostic pour les
systèmes à événements discrets est de détecter, à partir d'un flot
d'observations, si des erreurs se sont produites dans le système. Les
algorithmes de diagnostic doivent s'adapter à un contexte
d'observabilité réduite, où de nombreux événements ne sont pas
visibles par le superviseur. Vérifier l'observabilité et la
crucial et non trivial. MExICo s'intéresse aux aspects suivants :
- Diagnostic à base de dépliages
- Observabilité et diagnosticabilité
- Diagnostic décentralisé
- Test. Soit une spécification donnée par un modèle formel M et une
> implémentation I, supposée conforme à M ; le comportement de I est
> influencé par le flot des entrées reçues, et il n'est observable que
> via un flot de sorties. Le test de conformité consiste à construire,
> quand c'est possible, des flots d'entrées qui permettent de déterminer
> si I est conforme à M. MExICo s'intéresse au test des systèmes
> distribués asynchrones.
-
Dans le test asynchrone, un testeur centralisé envoie des
entrées non séquentielles et observe des sorties sur différents
ports sous forme d'ordres partiels.
- Dans le test local, plusieurs processus envoient des messages
de test à leurs voisins et observent localement les réponses ;
le problème de test consiste à déterminer la conformance globale
à partir des résultats locaux.
- Synthèse de contrôleurs. Dans un environnement distribué, il s'agit
de synthétiser un programme distribué ou des contrôleurs distribués
qui communiquent localement avec les composants du système. La
principale difficulté vient du fait que les contrôleurs (ou
programmes) ont seulement une vue partielle du système. Il est
essentiel de spécifier les propriétés directement en termes de
causalité en utilisant des modèles d'exécutions fondés sur les ordres
partiels comme les MSCs ou les traces de Mazurkiewicz.
- Adaptation et boîtes grises. Contrairement aux applications
monolithiques du passé, on observe que de plus en plus de services ne
sont plus fournis par un seul serveur mais par l'interaction et la
coopération de plusieurs composants spécialisés. Comme ces composants
ont des provenances diverses, on ne peut plus supposer que l'on a
accès à leur technologie interne (comme dans le cas des technologies
propriétaires). Ainsi, pour composer des services Web, pour déterminer
la violation de contrats ou de spécifications, pour adapter des
services existants à de nouvelles situations etc., on doit analyser
les interactions entre des composants dont on ne connaît que
l'interface publique, que l'on décrit comme des « boîtes grises ». On
voit apparaître trois points essentiels :
- l'abstraction
- la composition
- l'adaptation
- Domaines d'application
- Sécurité routière
- Adaptation pour la composition des services Web
- Télécommunications
Relations industrielles et internationales
- EMoTiCon: Equivalences between Models with Time and Concurrency.
Projet de l'institut Farman de l'ENS Cachan avec le LURPA (Laboratoire
Universitaire de Recherche en Production Automatisée).
- SMYLE: EGIDE/DAAD (Procope 2008/2009), avec Munich et
Aix-la-Chapelle, sur le passage des spécifications en MSCs aux modèles
de conception.
- Relations et échanges soutenus avec le Chennai Mathematical
Institute (CMI), Inde ; ARCUS.
- Projet ANR DOTS (distributed, open and timed systems) avec l'IRCCyN,
l'IRISA, le LaBRI et le LAMSADE.
- Participation au projet européen Disc (distributed supervisory
control of large plants) avec des partenaires académiques et
industriels en France, en Italie, aux Pays-Bas, en Belgique, en
Allemagne et en République Tchèque.
- Projet ANR Checkbound avec le LACL, le LAMSADE, le LIG, le LSV,
l'INT et le PRISM sur le model-checking pour la « performability » et
la sécurité des systèmes informatiques.
- Nombreuses coopérations académiques avec Leipzig, Duisburg, Padova,
Bordeaux, Milan etc.
