surete

surete/04_modeles_synchrones.md

@@ -0,0 +1,260 @@
+# Modèles synchrones
+
+## Motivations
+
+### Airbus
+
+- Logiciel critique
+- organisé en cycles
+- contraintes temporelles
+- grand volume de cde : 1 500 000 Lignes de Codes
+
+### Voitures modernes
+
+- bmw série 7 : 150 controleurs
+- ford f150 :   150 000 000 lignes de codes
+
+## Comment programmer un système réactif
+
+- un cycle d'exécution
+	- temps physique continu rendu discret dans le logiciel
+- des contraintes temporelles
+- système critique
+
+Boucle d'exécution répétée
+
+```
+    +---------------------+
+ .->|Environement physique| -.
+ |  +---------------------+  |
+ |                           |
+ |  +---------------------+  |
+ `- | Système de controle |<-.
+    +---------------------+
+```
+
+## Problématiques
+
+- comment gérer la concurrence ?
+- comment composer les composants du système ?
+- comment les cnotraintes temporelles sont implémentées ?
+
+## langages et modèles synchrones 
+
+### Qu'est-ce qu'un modèle synchrone
+
+Ce sont des modèles où une grande quantité de composants sont synchronisés par une horloge unique.
+
+Cette horloge dicte l'instant auquel les composants relèvent les valeurs mesurées pour continuer les calculs.
+
+### Diagramme de blocs
+
+Une description des controles et signaux du système très précis, modélisant graphiquement le cheminement d'un calcul
+
+```
+x -> b -> + -+-> y
+     z-1 -^  |
+     ^--- a<-+
+```
+
+rien n'es représenté en prennant en compte les artéfacts d'exécution (par exemple les erreurs de concurrences).
+
+### Lustre
+
+Inventé à Grenoble en 1987.
+
+Modélisation de code en portes de circuit logiques.
+
+```
+ init  --> +-------+
+ incr  --> | count | --> n
+ reset --> +-------+
+```
+
+```lustre
+
+node COUNT(init, incr: int; reset: bool) returns (n: int);
+let
+	n = init -> if reset then init else pre(n) + incr;
+tel;
+
+```
+
+Description des relations entre les paramètres d'un noeud du circuit.
+
+Plusieurs distrbutions :
+
+- SCADE (commercial) : Safety Critical Application Development Environment.
+	- utilisé par airbus, Dassault, Thales, schneider ...
+	- utilises le kernel LustreV6
+
+> note :
+> Nous nous concentrerons sur LUSTRE, contournant cet outil.
+
+## Lustre
+
+syntaxe
+
+```
+node <name-of-node> (<x_1>: <t_1>; ... <x_n>: <t_n>) returns (<y_1>: <t_1>; ... <y_n>: <t_n>)
+var <z_1>: <t_1>; <z_n>: <t_n>
+let
+	<equations>
+tel
+```
+
+Les équations sont des relations entre les paramètres et les valeurs déduites, retournées.
+
+```
+<equations> :=  A = (...)
+            :=  (A, B) = (...)
+```
+
+### Cycles d'exécution
+
+Il existe des déclanchements / triggers qui déclanchent :
+- lecture des entrée
+- calcul
+- écriture des sorties
+
+Les déclanchements ne sont pas réguliers.
+Chaque déclanchement est considéré atomique.
+- Le temps de calcul maximal doit être inférieur à l'interval minimul des déclanchements.
+
+```
+déclanchements :  R_1         R_2    R_3            R_4              R_5
+                   |           |      |              |                |
+temps de calcul :  |####       |#     |###           |##              |#
+temps :           -+-----------+------+--------------+----------------+-
+                    ^^^^\       ^^^^^^\
+                         \             \_ temps minimal entre deux déclanchement
+                          \______________ temps de calcul maximal
+```
+
+problème de synchronisation possible
+
+```
+h1 :         --|--|--|--|--|--|--|--|--|--|--|--|--|--|--|
+h2 :         --------|--------|--------|--------|--------|
+                                 |____/.    /__/|________/
+monde réel : --------------------*----------*---*---------
+                                m_1    .    m_2 m_3
+                                 .     .
+                                 ^\    ^\_ système utilisant h2 détecte l'événement m_1
+                                   \______ système utilisant h1 détecte l'événement m_1
+```
+
+### données
+
+- valeurs
+- variables
+- constantes
+
+### typages et horloges
+
+```lustre
+x:: . on True(b)
+y:: . on False(b)
+
+b :  True  True  True  False True
+    -|-----|-----|-----|-----|---
+x :  1     1     1     /     1
+y :  /     /     /     2     /
+```
+
+Quand l'événément False(b) est réalisé, la valeure de x est inexploitable.
+
+> note : 
+> un événement False(b) est utilisé comme horloge qui cadence la validité de la variable x.
+
+### Opérateurs
+
+
+- 'pre x'
+```
+        -|-----|-----|-----|-----|---
+x :      1     2     3     1     2
+pre x :  /     1     2     3     1
+```
+
+pre x correspond à une boucl rétro-active dans le système : il rammène un résultat vers une entrée.
+
+- 'a -> b'
+
+```
+         -|-----|-----|-----|-----|---
+a :       1     2     3     4     5
+b :       11    12    13    14    15
+a -> b :  1     12    13    14    15
+```
+
+c'est une initialisation à une certaine valeur, puis le suivi d'une loi.
+
+- 'x fby y'
+
+```
+          -|-----|-----|-----|-----|---
+a :        1     2     3     4     5
+b :        11    12    13    14    15
+a fby b :  1     11    12    13    14
+```
+
+c'est une initialisation avec un décalage pour lire la valeure de b passée.
+
+- 'merge c x y'
+
+```
+                   -|-----|-----|----
+c :                 True  False True
+x::. on c :         1     /     2
+y::. on False(c) :  /     10    /
+merge c x y :       1     10    2
+```
+
+agrégation de deux propriétés pour combiner leur temps de validité.
+
+- 'when'
+
+```
+           -|-----|-----|----
+b :         True  False True
+x :         1     2     3
+x when b :  1     /     3
+```
+
+- Opérateurs booléens conventionnels.
+- Interdiction de définition cycliques :
+	- x = x
+	- x = x + 1
+	- x = y ; y = x
+
+### Notes
+
+- Tout est borné en temps et en mémoire.
+- La causalité mathématique est respectée.
+- Beaucoup de checks de consistances sont possibles.
+- Formalisation sémantique simplifiée.
+
+
+### Exemples
+
+
+fonction qui retourne le maximum de a et b
+
+```lustre
+node (a, b: int) returns (out: int)
+let
+	out = if a < b then b else a;
+tel
+```
+
+fonction qui prends un nombre en paramètre et ne retourne uniquement si sa valeur est pair, sinon il retourne zéro.
+
+```lustre
+node (v: int) returns (out: int)
+var b: bool;
+let
+	b = (v mod 2) == 0;
+	out = merge b (v when b) 0;
+tel
+```