notes-ing2/surete/04_modeles_synchrones.md

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 --> +-------+

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

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

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.

node (v: int) returns (out: int)
var b: bool;
let
	b = (v mod 2) == 0;
	out = merge b (v when b) 0;
tel