Skip to content. | Skip to navigation

Emergences

Lettre d'information n° 28

Image emergences pour impression
Personal tools
You are here: Home 2013 Lettre d'information n° 28 Partenariat franco-indien sur les modèles formels
Document Actions

Partenariat franco-indien sur les modèles formels

Des chercheurs d'Inria développent une collaboration fructueuse avec deux instituts mathématiques du sud de l'Inde, pays qui vit naître le système décimal, le concept du zéro et les nombres négatifs voici quelques millénaires. Le partenariat ambitionne de fournir des outils de modélisation formelle et de vérification des systèmes distribués. Des avancées dans ce secteur permettraient, entre autre, d'améliorer la fiabilité des services web.

Des chercheurs d'Inria développent une collaboration fructueuse avec deux instituts mathématiques du sud de l'Inde, pays qui vit naître le système décimal, le concept du zéro et les nombres négatifs voici quelques millénaires. Le partenariat ambitionne de fournir des outils de modélisation formelle et de vérification des systèmes distribués. Des avancées dans ce secteur permettraient, entre autre, d'améliorer la fiabilité des services web.

Chennai. Anciennement Madras. 6 millions d'habitants. Le poumon économique du sud-est de l'Inde. Deuxième locomotive en technologies de l'information sur tout le sous-continent. Egalement un grand pôle universitaire, la ville compte deux instituts mathématiques : le Chennai Mathematical Institute (CMI) et l'Institute of Mathematical Sciences (IMSc). Depuis quelques années, ces deux entités renommées collaborent avec plusieurs établissements français, dont le centre Inria de Rennes. Les recherches communes portent sur la modélisation formelle et la vérification de systèmes distribués.

Mais, l'histoire débute en fait dans un troisième pays. Comme l'explique le chercheur Loïc Hélouët, “depuis plusieurs années, nous avions une collaboration avec NUS, l'université de Singapour. Et plus particulièrement avec le professeur P.S. Thiagarajan. Ce scientifique de grand renom est d'origine indienne. Par son intermédiaire, nous avons été mis en contact avec des chercheurs de Chennaï.”  En 2008, un quartet académique s'est finalement formé intégrant NUS, CMI, IMSc et Inria.

Équipe associée

Vecteur privilégié de cette collaboration : trois équipes associées successives. CASDS  en 2006-09. DST en 2009-11. Puis Distol (1), lancée début 2013. “Le cœur de ce nouveau projet porte sur la vérification et la supervision de systèmes distribués à travers la modélisation formelle et le raisonnement automatique sur les modèles. Notre objectif est de garantir le bon fonctionnement d'un système. Très souvent, les programmeurs commencent à écrire du code sans construire un modèle du système qu'ils développent. Nous sommes convaincus que cet effort de modélisation est essentiel. Il permet de raisonner sur un système et d'analyser sa correction avant de se lancer dans sa programmation. On peut ainsi éviter des dysfonctionnements qui ne sont pas dus à des erreurs de développement mais plutôt à la conception elle-même du système. Développer sans modèle fonctionne très bien... jusqu'au jour du premier vrai bug.” Pour les industriels et les éditeurs de logiciels, de telles défaillances peuvent  prendre une tournure catastrophique. Pas facile en effet de détecter un bug résultant d'une erreur de conception en inspectant du code. Pas facile non plus de le circonscrire. Parfois même, il n'est d'autre choix que de se résoudre à... une complète remise à plat de la conception du système. Et cela en remettant en cause tous les choix faits depuis le début du projet.

Déplacement vers les services web

Alors que le pivot de cette collaboration se déplaçait vers l'Inde, son thème principal, lui aussi, a notablement évolué. “Au départ, nous étions centrés sur des modèles et techniques de vérification pour les protocoles de télécommunications. Puis nous avons commencé à cheminer vers le domaine des services web. Fait assez remarquable, nous sommes arrivés séparément à la même conclusion dans nos équipes respectives. Dans les dernières décennies, on est passé d'un monde où le défi majeur des méthodes formelles consistait à vérifier des protocoles, à un monde où les moyens de communication sont supposés acquis, et où la grande question devient d'assurer la correction d'applications distribuées, notamment au-dessus du web. Une grande partie de notre communauté en arrive d'ailleurs à cette conclusion.

De fait, “déployer des logiciels sur l'immensité du web engendre quantité de problèmes. Des questions d'échelle et d'hétérogénéité... Sur le web, beaucoup d'applications utilisent des services fournis par des tiers. Des services bancaires par exemple. On peut intégrer de tels services dans une application sans forcément maîtriser complètement leur domaine d'expertise. On fait simplement de la sous-traitance au fournisseur d'une solution logicielle. Conséquence : on se retrouve alors avec un système ouvert dans lequel certaines parties sont complètement opaques et vues comme des interactions avec le reste du monde.”  Mais de telles architectures composites appellent elles aussi l'utilisation de techniques de vérification formelle, pour s'assurer que les composants interagissent bien, mais aussi que le système ainsi assemblé est correct, pour peu que les sous-traitants respectent leur cahier des charges.

De grands bénéfices

Comme le souligne Loïc Hélouët, les techniques de raisonnement formel peinent encore à percer dans l'industrie. “Ces compétences tendent à rester confinées dans les laboratoires, ce que je regrette. En effet, on peut en tirer de grands bénéfices. Quand on y met le prix et l'énergie, l'utilisation de modèles formels... cela paye !  Hélas, pour l'instant, ni nous, ni nos homologues indiens ne sommes parvenus à trouver un partenaire industriel à qui nous pourrions transférer toute notre expérience des modèles. Voici d'ailleurs un des dangers qui guettent notre communauté : nous pourrions fort bien rester dans notre tour d'ivoire jusqu'à la fin des temps à produire des prototypes de recherche qui finalement ne seraient d'aucun usage pour la société. Cela n'aurait pas de sens de produire des résultats mathématiques difficiles si nos modèles ne trouvaient pas d'utilisation réelle.”  Un défi supplémentaire s'ajoute donc à la liste des scientifiques : convaincre les industriels que la modélisation formelle permet de concevoir des systèmes plus robustes et de débusquer plus facilement les bugs. Et qu'il faut donc la considérer comme une partie essentielle du développement de systèmes logiciels.


-----
Note :
(1) Distol signifie: Distributed Systems, Stochastic Models and Logics. Trois équipes Inria basées à Rennes participent actuellement à cette collaboration : Distribcom, Sumo and S4.