Départements de recherche

VESONTIO


Équipe VESONTIO

Responsable

Pierre-Cyrille HÉAM

Contexte

VESONTIO (Vérification et Validation de logiciels et de systèmes embarqués) est le nom que porte l’équipe depuis 2008, avant quoi elle était appelée TFC (Techniques Formelles et à Contraintes). Une partie de l'équipe est par ailleurs intégrée au projet bi-localisé (Nancy, Besançon) INRIA CASSIS.

La compétence spécifique de l'équipe est la combinaison de méthodes (preuve automatique, model-checking, test) pour la vérification et validation à base de modèles, le verrou scientifique étant l'explosion combinatoire de la taille des modèles des systèmes à analyser. Cette activité est menée suivant trois directions : modélisation de systèmes finis de grande taille et de systèmes infinis, vérification et validation automatique à base de modèles, y compris la génération de tests, passage à l'échelle.

Objectifs et Thématiques scientifiques

L’équipe a porté des efforts spécifiques sur la modélisation, vérification et validation automatique de systèmes embarqués (ex : cartes à puce et automobile), systèmes à base de composants et de services, ainsi que sur l'étude de la sécurité et de sûreté de systèmes de communication et d'information.

Compte tenu de l'évolution thématique, en particulier vers les micro-systèmes, de nouveaux défis scientifiques ont été identifiés :
- Gérer la complexité par construction
- Gérer les systèmes hétérogènes à composants
- Gérer l'incertitude par adaptation/reconfiguration

Aussi, ressortent de ces enjeux scientifiques, deux thèmes de recherche :

› Sécurité et fiabilité des communications et des systèmes d'information : élaboration de méthodes formelles pour vérifier et tester la sécurité de systèmes de communications, comme les protocoles, ou des systèmes d'information. Cette problématique est abordée à la fois par des techniques de vérification sur des modèles symboliques (langages, automates, logiques, réécriture, etc.), mais aussi de test à partir de modèles (couverture du modèle, scénario, etc).

› Vérification et test de composants logiciels et de systèmes embarqués : conception, modélisation de systèmes fiables et sécurisés. Les approches utilisées sont d'une part les techniques de vérification des systèmes composés (réseaux de Petri, automates d'interfaces, etc.) et de test à partir de modèles (couverture de modèle, test au limite, etc).

Savoir-faire

L’un des points forts de l’équipe VESONTIO est de regrouper, au sein d'une même équipe, des compétences dans différents domaines de l'analyse de la fiabilité logicielle : model-checking, preuve et test s'appuyant sur des modèles.

Cet éclectisme permet des combinaisons d'approches originales pour attaquer de façons conjointes et complémentaires des défis communs. Le transfert technologique vers l'entreprise Smartesting donne lieu à de nombreuses collaborations industrielles sur les thématiques de l'équipe.

Mise en œuvre

Dans le cadre des échanges inter-départements de FEMTO-ST, sont apparus des besoins de modélisation, test et simulation de systèmes complexes, à différentes échelles. Ces derniers comportent à la fois des aspects logiciels, mais aussi des phénomènes physiques, de type mécanique, énergétique ou quantique par exemple. Plusieurs travaux en collaboration avec d'autres départements de FEMTO-ST ont été menés dans cette direction.