Vérification formelle d'un générateur de code pour un langage synchrone – VeriSync

Le projet proposé ici a pour but d'améliorer considérablement la
sûreté de logiciel embarqué qui est développé dans le contexte de
l'Ingénierie Dirigée par les Modèles. Ce but est atteint par une
preuve formelle de la correction de transformations essentielles qui
interviennent lors de sa compilation vers du code exécutable.

Le projet cible la compilation d'un langage synchrone vers un
langage de programmation impératif. Des langages synchrones sont
un formalisme expressif pour des algorithmes embarqués, et sa
sémantique précise les rend particulièrement appropriés pour notre
but. Nous avons prévu d'étendre le noyau du formalisme avec de
l'information quantitative et de prendre en compte cette information
lors des transformations, pour ainsi rendre l'approche utilisable pour
le développement de systèmes temps-réel.

La définition de la sémantique et la preuve de correction du
compilateur seront fait dans l'assistant de preuve interactif
Isabelle. Le compilateur sera exécutable et sera évalué sur des
exemples réalistes.

Ceci est un projet de recherche fondamentale et n'a pas vocation à
fournir un produit immédiatement utilisable dans un contexte
industriel. Cependant, la motivation pour ce projet émane de projets
implicant des acteurs importants du domaine embarqué et auxquels les
partenaires sont associés. Les résultats seront ré-injectés dans des
projets d'envergure industrielle.