Modèles et langages pour la programmation des systèmes réactifs |
La programmation parallèle et réactive touche désormais tous les domaines de l’informatique: contrôle en temps réel de systèmes embarqués (avions, voitures, train), interfaces graphiques, réseaux de capteurs, tradding algorithmique, chatbots, etc. Elle se fait aujourd’hui avec des langages de programmation dédiés permettant d’écrire une spécification mathématique du système qui sert de référence pour la simulation, le test, la vérification formelle et qui est compilée vers du code exécutable. C’est l’approche d’outils très utilisés tels que Simulink/Stateflow et Scade. Mais plus largement, les langages généralistes intègrent maintenant des constructions pour programmer des applications réactives.
Quels sont les principes de ces langages et leur sémantique, comment sont-ils implémentés et vérifiés? Comment garantir des propriétés de sûreté essentielles, e.g., l’absence de blocage (deadlock), le déterminisme ou encore une exécution en temps et mémoire bornés? L’objectif de ce cours est l’étude et la mise en oeuvre des principes et modèles fondamentaux utilisés pour concevoir et réaliser les systèmes réactifs; les différents modèles de composition et de temps, l’expression de modèles mathématiques dans des langages de haut niveau (e.g., langages synchrones, langages de modélisation hybride), la spécification de propriétés (e.g., logique temporelle, observateurs) pour la vérification et le test, les méthodes de validation par simulation, test et vérification formelle et les étapes de compilation vers une cible séquentielle et parallèle et dont on peut montrer la correction vis-à-vis du modèle.
Le cours est illustré à l’aide d’exemples écrits dans des langages de programmation. On utilisera en particulier des langages fondés sur le parallélisme synchrone: le langage ReactiveML, Lustre, et Zelus ainsi que des outils de vérification par model-checking: Kind2 et Cubicle.
Le cours comporte un aspect fortement pratique dans les TD/TPs pour mettre en oeuvre des points du cours. Un projet de programmation ambitieux sera proposé (par ex., la programmation d’un drone, d’un arduino ou l’écriture d’un compilateur d’un langage dédié).
Modalités de contrôle des connaissances : Projet Format du cours : cours présentiel, hybride si nécessaire.
This document was translated from LATEX by HEVEA.