Marc Pouzet, DIENS, ENS Paris et INRIA équipe PARKAS

Le fichier kahn.hs et le fichier kahn_lazy.ml de la démo (transparent 27/45).

Résumé. On trouve aujourd’hui du logiciel temps réel dans les avions, les trains et les voitures. E.g., commandes de vol, système de freinage et contrôle moteur d’avion; contrôle de bord et gestion de la position d’un train; gestion de l’énergie d’une voiture électrique, pour n’en citer que quelques uns. Ce logiciel est complexe — quelques millions de lignes de code pour les commandes de vol d’un avion moderne — et il est difficile à concevoir ou à tester car il interagit avec un environnement physique qui n’est connu que partiellement. Enfin, il doit répondre à des exigences de sûreté rigoureuses et vérifiables par des autorités indépendantes, comme l’imposent l’avionique civile et le ferroviaire, par exemple.

La science informatique s’est intéressée dès la fin des années 70 à cette question essentielle: comment programmer le logiciel temps réel et dans quel langage afin que le programme soit précis, qu’il autorise des raisonnements formels indépendants de toute implémentation et que le code produit par le compilateur soit correct, qu’il s’exécute de manière déterministe, sans blocage et respecte les contraintes de temps réel?

Dans cet exposé, nous montrerons la genèse du modèle de programmation synchrone jusqu’à son utilisation aujourd’hui pour développer de nombreux logiciels d’applications temps réel critiques.

Nous rappellerons sa filiation avec les modèles et outils anciens de l’automatique ainsi que ceux de la théorie des langages, les principes du modèle et son intégration dans plusieurs langages dédiés.

Nous montrerons quelques unes des questions de recherche qui se sont posées et les évolutions majeures que les langages synchrones ont connu.

Nous montrerons deux pistes de recherche plus récentes. L’une est le développement d’un compilateur d’un langage synchrone réaliste avec une preuve formellement vérifiée que le code produit est correct vis-à-vis du code source. L’autre vise à étendre l’expressivité du langage pour décrire des systèmes hybrides combinant du temps discret et du temps continu, en particulier l’interaction entre le logiciel et son environnement physique. On vise ici l’écriture de modèles que l’on pourra tester et valider avec une plus grande fidélité vis-à-vis du système réel final.