Description

Avec la démocratisation des appareils interactifs, les utilisateurs s'attendent désormais à interagir avec leurs systèmes par le biais d'interactions tactiles et avancées. Pour faciliter la mise en œuvre de ces systèmes, des langages de programmation dédiés « orientés interaction » ont été proposés. Ces langages permettent de décrire efficacement à la fois l'apparence du système et son comportement interactif. Ils sont de plus en plus populaires, y compris pour le développement de systèmes critiques. Cependant, peu d'efforts ont été consacrés à la formalisation de ces langages, de leur sémantique ou de leur modèle d'exécution.

L'objectif de ce projet de recherche est de formaliser Smala, un langage orienté interaction développé à l'ENAC.
Smala est un langage réactif, dans lequel le programmeur spécifie la façon dont les événements extérieurs sont propagés et dont le programme réagit, en mettant à jour son état interne et en déclenchant des comportements observables. Ce programme déclaratif de haut niveau peut ensuite être compilé en code impératif qui implémente ces réactions.

Au cours de ce projet, le candidat formalisera le langage et sa sémantique, et implémentera sa compilation vers le langage de bas niveau C. Une partie importante du travail sera consacrée à la vérification de bout en bout du schéma de compilation : le candidat développera une preuve mécanisée que le programme C généré implémente bien le comportement spécifié par le programme source Smala.

Pour ce faire, le candidat utilisera principalement l'assistant de preuves interactif Rocq. En effet, celui-ci comprend des fonctionnalités pour la spécification (de la sémantique de Smala), l'écriture de programmes (le schéma de compilation en tant que programme purement fonctionnel) et les preuves vérifiées automatiquement (relant cette sémantique, la fonction de compilation et la sémantique du C telle que spécifiée dans le projet CompCert).

Compétences requises

Le candidat doit être titulaire d'un master (ou équivalent) en informatique. Le candidat doit être familiarisé avec • les méthodes formelles • le prouveur Rocq • la programmation OCaml • la compilation De plus, une connaissance de la programmation IHM et/ou des systèmes de gestion du trafic aérien sera appréciée.

Bibliographie

[1] Philippe Antoine and Stéphane Conversy. “Volta: The First All-Electric Conventional Heli-
copter”. In: MEA 2017, More Electric Aircraft. Bordeaux, France, Feb. 2017. url: https :
//enac.hal.science/hal-01609233.
[2] Albert Benveniste and Gérard Berry. “The Synchronous Approach to Reactive and Real-Time
Systems”. In: Proceedings of the IEEE 79.9 (Sept. 1991), pp. 1270–1282. url: https : / /
ptolemy.berkeley.edu/projects/chess/design/2010/discussions/Pdf/synclang.pdf.
[3] Timothy Bourke, Basile Pesin, and Marc Pouzet. “Verified Compilation of Synchronous Dataflow
with State Machines”. In: ACM Trans. Embed. Comput. Syst. 22 (5s Sept. 9, 2023), 137:1–
137:26. issn: 1539-9087. doi: 10.1145/3608102. (Visited on 11/19/2024).
[4] Lélio Brun. “Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Lan-
guage with Reset”. PhD thesis. PSL Research University, June 2020. url: https://theses.
hal.science/tel-03068862/.
[5] Xavier Leroy. “Formal Verification of a Realistic Compiler”. In: Communications of the ACM
52.7 (July 2009), pp. 107–115. issn: 0001-0782, 1557-7317. doi: 10.1145/1538788.1538814.
[6] Mathieu Magnaudet et al. “Djnn/Smala: A Conceptual Framework and a Language for Interaction-
Oriented Programming”. In: Proc. ACM Hum.-Comput. Interact. 2 (EICS June 19, 2018), 12:1–
12:27. doi: 10.1145/3229094.
[7] Basile Pesin, Celia Picard, and Cyril Allignol. “Reactive Semantics for User Interface De-
scription Languages”. In: Proceedings of the 18th Interaction and Concurrency Experience (to
appear). Lille, France, 2025.
[8] Daniel Prun and Pascal Béger. “Formal Verification of Graphical Properties of Interactive
Systems”. In: Proceedings of the ACM on Human-Computer Interaction 6 (EICS June 14,
2022), pp. 1–30. issn: 2573-0142. doi: 10.1145/3534521.
[9] The Coq Development Team. The Coq Proof Assistant. Version 8.20. Zenodo, Sept. 4, 2024.
doi: 10.5281/zenodo.14542673

Mots clés

Informatique, Compilation, Méthode Formelle, Interaction, Langage de Programmation