Programmation synchrone

Système réactif

Heptagon installé : heptc

Ce qu’on a appris jusqu’ici

• Programmation (langages)
  • OCaml, C, C++, Python
• Algorithmique
  • Modèle et Spécification, tris, graphe
• Programmation transformationnels (par opposition à réactif) (merci Zohar Manna et Amir Pnueli)
  • aka lis une entrée, calcule et produis une sortie
  • Exemple transformationnel : sort (UNIX), gcc

Programmation réactive

Exemple réactif

• Pilote automatique
  • Depuis les années 80 : il y a une assistance automatique en permanence pendant un vol d’avion, même lorsqu’on est en mode manuel (fly-by-wire).
• Modem
• Four sophistiqué
• ABS

Caractéristiques essentielles des systèmes réactifs

• Criticité
  • Coût démesuré (vies humaines)
  • Exemple : Vol 501 d’Ariane V (coût : centaine de millions d’euros)
    • L’institut INRIA a participé aux réunions concernant cet événement.
  • Exemple : Machine Therac-25 : 6 irradiations massives, trois mortels
  • En général :
    • Aéronautique (fly-by-wire)
    • Médical (radiothérapie) : pompes à insuline, pacemaker…
    • Militaire (guidage des missiles…)

Dans le logiciel critique, il faut faire “ceinture et bretelle”.

• Temps-réel : réagir dans un intervalle de temps fixé
  • Exemple : TCAS-II

Correction temporelle \leftrightarrow correction fonctionnelle \RA il y a des cas où ça va ensemble

• Mathématiques dédiées
  • Systèmes dynamiques
  • Automatique (+ appliquée que les systèmes dynamiques) \RA Control Theory // sous-texte du cours

Mathématiques nées avec la révolution industrielle

Exemple : Régulateur à boules de Watt

• Contraintes de ressources
  • Matériel informatique dédié embarqué : contraintes de performances, de batterie (énergie), en espace (mémoire), de temps (lié à l’aspect algorithmique)
  • Lié à la compilation, au système d’exploitation, etc.

Langages synchrones

Langages spécialisés pour la programmation des systèmes réactifs

Objectifs

• Aider la programmation à un haut niveau de sûreté
• Faciliter le respect des contraintes temps réel
• Proche des mathématiques dédiées (proche du concept de l’automatique)

\RA Idée sous-jacente : Notion de temps logique, discret et global

Langages conçus en France : à Grenoble (notamment), Nice, Rennes et Paris.

Schéma-bloc

Utilisés pour palier les besoins des ingénieurs avec un background “automatique” vers le code C

• On programmait directement avec les dessins, un fil = une suite infinis de données
• SCADE 6 était un programme pour ça, c’était un peu comme un compilateur en somme

Heptagon : la programmation synchrone a flots de données

Cf. Dossier de code

Exécution cyclique à 3 phases :

• Lecture (capteurs/état)
• Calcul
• Écriture (actionnaires/état)

A la fin de développement : vérification des contraintes temporelles.

On programme dans un langage avec un temps logique et un temps discret.

On considère qu’entre le début et la fin du cycle, aucun temps ne s’est écoulé, afin que l’environnement n’ait pas le temps de changer.

D’un certain point de vue, on peut représenter un programme synchrone comme une machine à état / un automate (à mémoire) finie et déterministe. Notre automate, en plus d’avoir des entrées, possède des sorties, c’est un transducteur.

Pour prouver si deux automates sont égaux, on peut faire une bisimulation.

Une bisimulation est une relation R \subseteq S \times S tel que \forall (s_{1}, s_{2}) \in R, on a :

1. s_{1} final \Leftrightarrow s_{2} est final
2. Si s_{1} \xrightarrow{a} s_{1}', il existe s_{2}' tel que s_{2} \xrightarrow{s_{2}'} et (s_{1}', s_{2}') \in R
   
3. si s_{2} \xrightarrow{a} s_{2}', il existe s_{1}' tel que s_{1} \xrightarrow{a} s_{1}' et (s_{1}', s_{2}') \in R

Théorème : deux états finaux s_{1} et s_{2} reconnaissent le même langage ssi il existe une bisimulation R telle que (s_{1}, s_{2}) \in R

Exemple :
Bisimulation : R = \{ (x, u)_{x}, (y, v)_{x}, (y, w)_{x}, (z, w)_{x}, (z, v)_{x} \}

Exemple transducteur :