L'outil TINA.tedd du LAAS lauréat

Pour sa 3ème participation au MCC (Model-Checking Contest,), l'outil TINA.tedd, développé par l'équipe Vertics du LAAS/CNRS, s'est classé premier dans la catégorie "StateSpace". Les épreuves consistent à explorer de manière efficace l'espace d'état de réseaux de Petri, c'est-à-dire l'ensemble des configurations différentes susceptibles de se produire pendant l'exécution. Ces espaces d'états ont une taille allant de 10^6 à plus de 10^130 éléments ; chaque espace doit être exploré intégralement en moins d'une heure, et sa taille exacte doit être calculée, à un élément près. L'enjeu du concours est de contribuer à améliorer les performances de ces outils dits de "model-checking" afin qu'ils puissent passer à l'échelle sur de plus en plus de cas d'étude.

 

Les réseaux de Petri sont un modèle théorique largement utilisé pour modéliser de manière mathématique les chaînes de production, les tâches logicielles concurrentes, les protocoles, les systèmes distribués, etc. L'équipe Vertics du LAAS/CNRS s'intéresse entre autres à une extension des réseaux de Petri avec la prise en compte de la dimension "temps"



Personnes impliquées dans TINA.tedd:

  • Bernard Berthomieu
  • Silvano Dal Zilio
  • Didier Le Botlan