260 lines
6 KiB
Markdown
260 lines
6 KiB
Markdown
# 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
|
|
```
|