L’équipe COSMO (COmmunications Spécifications MOdèles) étudie les propriétés fondamentales des systèmes informatiques et biologiques et, plus généralement, le comportement de systèmes dynamiques réactifs, décentralisés et ouverts. Dans ce cadre, elle s’intéresse à la spécification et à l’analyse de ces systèmes, ainsi qu’à leur conception. L’équipe se caractérise par une continuité entre les recherches fondamentales et appliquées, avec des avancées théoriques significatives, des développements méthodologiques, la production d’outils logiciels, des applications à des problèmes réels, jusqu’à la création de liens industriels. Deux orientations structurent la recherche au sein de l’équipe.

1. Une problématique applicative axée sur les problèmes de société (médecine personnalisée, véhicule du futur, Internet du futur, …) et pour lesquels la définition de nouveaux cadres théoriques ou méthodologiques est nécessaire.

2. Des travaux ancrés sur une théorie « cœur de compétence » qui peuvent avoir des retombées dans la première orientation et y trouver leur application. Cette double orientation favorise la production d’outils logiciels et méthodologiques, à la fois pour permettre l’application et comme validation de la théorie.

Modélisation et analyse formelles, preuve, réseaux de Petri, algèbres de processus, réseaux booléens, réseaux d’automates, logiques modales, méthodes de tableaux, simulation entité-centrée, médecine personnalisée de précision, véhicules autonomes communicants, biologie des systèmes, Internet du futur, réseaux autonomiques, multi-agents

Dans le domaine de la médecine personnalisée et de précision, un des objectifs majeurs est la conception de logiciels d’assistance à la prise de décision pour le diagnostic et la thérapie. Dans cette perspective, la question centrale est la carence de méthodes pour interpréter les données de l’« omique ». En nous focalisant sur la prédiction de cibles thérapeutiques fondées sur l’analyse de réseaux moléculaires, nous avons formalisé les cadres théoriques adaptés afin d’inférer les cibles causales responsables de transition phénotypiques (sain/malade). Notre méthodologie a été implantée dans un ensemble d’outils logiciels s’appuyant sur la théorie des jeux et sur des principes d’abduction appliqués aux réseaux booléens.

Nous avons par ailleurs travaillé sur la modélisation, la simulation et la vérification formelles de modules de décision de véhicules autonomes et communicants. Nous avons proposé dans ce cadre une modélisations originale, scalable et paramétrique en automates temporisés et également un modèle de simulation multi-agent, les deux permettant d’évaluer les aspects de sécurité, de fluidité et de confort de diverses politiques de décision. Nous avons montré en particulier, en développant une comparaison entre ces deux approches, quel impact avait le niveau d’abstraction choisi sur les indicateurs considérés. Notre méthode de simulation a été implantée dans un plugin pour le simulateur Gama.

Nous nous sommes aussi intéressés aux technologies Cloud Computing et IoT (Internet of Things) dans le cadre de l’Internet du Futur. Le déploiement de ces technologies introduit de nombreux problèmes ayant une grande complexité. Nous avons alors proposé plusieurs approches pour modéliser ces problèmes de manière à relaxer certaines contraintes par une meilleure compréhension des spécificités de ces technologies et de leur utilisation. Nous avons par ailleurs adressé le problème du contrôle holistique et autonomique d’un environnement convergeant « Cloud IoT » satisfaisant les exigences de délai et de ressources de traitement pour la collection des données à partir de milliers de capteurs potentiellement déployés dans l’environnement. Enfin, nous avons proposé un modèle à base de réseaux de Petri des mécanismes autonomiques pour gérer l’élasticité des ressources dans le Cloud, dont l’analyse a été conduite grâce à notre outil SNAKES.

D’autres applications ont été abordées. En particulier, nous avons proposé un cadre formel de modélisation et d’analyse de systèmes de stockages distribués, par exemple les hiérarchies de caches dans des architectures de calcul haute performance, en collaboration avec le CEA. Plus récemment, une collaboration avec l’INRA Montpellier a été entamée sur la modélisation et l’analyse d’écosystèmes.