Les algorithmes distribués : un terrain de jeu formidable pour la vérification
Les systèmes informatiques répartis sont de plus en plus présents, dans notre vie quotidienne, comme dans des technologies avancées. Les erreurs dans les algorithmes distribués peuvent avoir des conséquence lourdes sur le plan humain et financier. Il est donc crucial de mettre au point des techniques rigoureuses de vérification de leur correction. La vérification de modèles est une approche des méthodes formelles qui date des années 1980. Elle a été appliquée avec succès à la vérification de matériel d’abord, puis de logiciel. Les systèmes répartis soulèvent de nouveaux défis pour la communauté de la vérification de modèles, et demandent de développer de nouvelles techniques et de nouveaux outils de vérification. En particulier le paradigme de vérification paramétrée et en plein essor pour aider à la vérification automatique de la correction des algorithmes distribués. Cet exposé présentera des développements récents en vérification paramétrée pour la validation d’algorithmes distribués.