Vers la vérification de SMALA, un langage réactif interactif

SMALA est un langage reactif dediea la programmation de systemesa forte composante interactive. Pour pouvoir utiliser ce langage dans un con-texte critique, il est necessaire de pouvoir apporter des garanties. Ainsi, nous nous interessonsa la verification formelle du compilateur de SMALA, avec pour objectif de garantir la preservation de la semantique du programme sourcea la compilation. Dans un premier temps, nous avons limite notre etudea un sous-ensemble de SMALA. Dans cet article, nous presentons une version preliminaire de la semantique operationnelle de ce sous-ensemble.