VERIMAG.

Les travaux de VERIMAG visent à produire des outils théoriques et des techniques pour permettre le développement de systèmes embarqués de qualité maîtrisée, et ce à des coûts compétitifs. Pendant ces dix dernières années, VERIMAG a contribué activement au développement de l'état de l'art en matière de spécification, vérification, et test de systèmes temps-réels synchrones et asynchrones. De fortes compétences ont été ainsi acquises par le laboratoire en terme de sémantique des langages temps-réels et de techniques de base pour la vérification (model-checking, analyse statique, abstraction, etc.). Les résultats obtenus trouvent de nombreuses applications industrielles, notamment dans les langages et outils pour le développement des logiciels et systèmes critiques et/ou embarqués.

VERIMAG a notamment développé Kronos, un outil de référence pour le model-checking de propriétés temps-réel, l'environnement IF, une plate-forme ouverte pour la validation de système temporisés asynchrones, et a contribué (en collaboration avec l'équipe Vertecs de l'IRISA) au développement de TGV, un outil de génération automatique de tests de conformité.

Le projet DYNAMO se situe dans le prolongement des recherches menées actuellement à VERIMAG, notamment dans le cadre des projets Expresso (RNTL) sur l'ordonnancement des programmes Java temps-réel et ADVANCE (Européen IST) sur la vérification de systèmes infinis. Cette activité fait partie des travaux de thèse de plusieurs doctorants à VERIMAG (Chaker Nakhli, Moussa Amrani) et du programme de recherche de Radu Iosif, récemment recruté comme CR CNRS.