Context

Le langage GAL (http://ddd.lip6.fr/gal.php ) permet d’exprimer la sémantique de systèmes concurrents. Il sert déjà de cible dans plusieurs transformations de modèle depuis des formalismes répandus (automates temporisés de Uppaal, Promela, reseaux de Petri...). Ce langage permet l’analyse par model- checking de propriéteés de logique temporelle (CTL, LTL) à l’aide d’un moteur de vérification basé sur des diagrammes de décision. L’objectif du stage est de développer un nouveau moteur de vérification appuyé par une transformation des modèles GAL vers une spécification exprimée en SMT (dans le langage SMTlibv2). Les solvers SMT (tels que Z3 de Microsoft) jouissent d’un grand pouvoir d’expression et offrent une solution performante (particulièrement en mémoire) pour la résolution de problèmes complexes (polynomiaux de degré élevé voire NP typiquement).

Un prototype de transformation existe déjaà, mais il ne supporte qu’un fragment du langage GAL, et il faut donc l’étendre. L’objectif du stage est de réussir à analyser une spécification GAL assez complexe (plus de 1000 lignes) qui modèlise le protocole de cohérence de cache appelé DHCCP de l’architecture TSAR. Ce modèle développé au cours d’un précédent stage, pourra au besoin être étendu pour couvrir des mécanismes non modélisés (éviction de cache...). On construira une évaluation des performances et du passage à l’échelle de la solution SMT face à la solution existante.

Dans un deuxième temps, et selon les résultats obtenus, la transformation qui est actuellement limitée aux propriétés d’accessibilité sera modifiée pour permettre la vérification de propriétés plus complexes (LTL). Si la réalisation est de bonne qualité elle pourra être intégrée aux outils existants et distribuée publiquement. (Stage pouvant donner lieu à une poursuite en thèse.)

Lieu : Equipe MOVE

Encadrants : Yann Thierry-Mieg, Quentin Meunier, Souheib Baarir