Logo equipe MeForBio

Méthodes formelles

Présentation

Les membres du thème méthodes formelles s’intéressent à la modélisation rigoureuse (mathématique) des systèmes, à la vérification automatique ou semi-automatique de leur correction, et à la synthèse de systèmes corrects par construction.

En particulier, pour les systèmes dans lesquels le temps doit être pris en compte explicitement, des formalismes comme les réseaux de Petri temporels ou les automates temporisés sont utilisés.

Parmi les thèmes récents étudiés figurent les systèmes temporisés répartis et l’exploitation de la concurrence, ainsi que les systèmes temporisés paramétrés. Ces derniers permettent de modéliser un système en laissant certaines grandeurs temporelles (délai de transmission, période d’activation, etc.) non spécifiées et c’est le processus de vérification qui déterminera l’ensemble des valeurs possibles permettant de satisfaire les propriétés désirées.

Valorisation

Un outil, appelé Roméo http://romeo.rts-software.org, permet la mise en oeuvre des techniques développées dans le cadre des travaux effectués sur le thème méthodes formelles.

Roméo permet notamment la modélisation de systèmes à travers un langage proche des réseaux de Petri temporisés, l’utilisation de paramètres temporels, la modélisation de préemptions, et la vérification de propriétés exprimées dans une logique temporelle temporisée et paramétrée.

Roméo est utilisé de façon pédagogique pour plusieurs cours de niveau master 2 mais aussi dans le cadre de collaborations industrielles :

    • Sodius: vérification d’un langage de spécification de haut-niveau (EFFBD)
    • BA Systèmes : routage d'AGV
    • Dassault Aviation

 

Logo-cnrsLogo-AtlanSticLogo-UniversiteNantesLogo-MinesNantesLogo-CentraleNanteslunamCOMUE