Département 2 : Méthodes formelles

Responsable de l’équipe : Steve Kremer
Tél. : +33 3 54 95 86 60
Mail : steve.kremer@loria.fr

Présentation

L’objectif du projet est la conception et la réalisation d’outils pour vérifier la sûreté des systèmes à nombre infini d’états. Notre analyse des systèmes se fonde sur une représentation symbolique des ensembles d’états comme langages formels ou formules logiques. La sûreté est obtenue par la preuve automatique, l’exploration symbolique de modèles, ou la génération de tests. Ces méthodes de validation sont complémentaires mais s’appuient, dans notre projet, sur l’étude de problèmes d’accessibilité et leur réduction à des résolutions de contraintes.
Une originalité du projet réside dans sa focalisation sur les systèmes infinis, paramétrés ou de grande taille, sur lesquels chaque technique prise séparément montre ses limites. Comme exemples de tels systèmes nous pouvons citer les protocoles opérant sur des topologies de taille arbitraire (réseaux en anneaux), les systèmes manipulant des structures de données de taille quelconque (ensembles), ou dont le contrôle est infini (automates communicants par tampon non borné).
Les applications visées ou en cours sont les logiciels embarqués par exemple sur cartes à puce, les protocoles de sécurité et les systèmes répartis.

Axes thématiques

• Déduction automatisée
• Vérification des protocoles de sécurité
• Service Automated Computing

Logiciels

• CI-Atse

• AVANTSSAR Orchestrator
• P2PEdit
• DeSCal

Collaborations

• Université de Clarkson
• Université de Genève
• Université de Vérone
• Université de Milan
• Équipe DAHU (INRIA Saclay, LSV et ENS Cachan)
• Université de Bristol
• Université d’Edimbourg
• Université de Kiel
• Université d’Albany (USA)
• France Télécom R&D
• Équipe MADYNES, SECSI et SCORE
• IRIT de Toulouse

Mots-clés

Méthodes formelles, déduction automatique, vérification automatisée, sécurité, systèmes embarqués, protocoles cryptographiques, Web services, modèles symboliques, modèles computationnels, génération de tests, procédures de décision, logique équationnelle, résolution de contraintes, automates