Vous êtes ici
VESONTIO
Contexte
VESONTIO (Vérification et Validation de logiciels et de systèmes embarqués) est le nom que porte l’équipe depuis 2008, auparavant elle était appelée TFC (Techniques Formelles et à Contraintes).
L'équipe VESONTIO est spécialisée dans la qualité logicielle et développe des travaux pour améliorer ou analyser la fiabilité, la sécurité ou la performance des systèmes. Les approches s'appuient sur des modélisations formelles tant des systèmes étudiés que des spécifications. Dans cette chaîne, un premier axe de travail autour de la modélisation formelle et semi-formelle en vue d'une analyse concentre des travaux notamment autour de SysML et des systèmes composites. Un deuxième axe fort étudie comment tester efficacement et automatiquement les systèmes. Enfin, un troisième axe autour de la vérification ou preuve automatique est développé, avec récemment des premiers résultats sur les programmes quantiques.
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 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.