From 489535501ed544c89d400b5c8b0607e90571617b Mon Sep 17 00:00:00 2001 From: JOLIMAITRE Matthieu Date: Sun, 10 Mar 2024 21:34:20 +0100 Subject: [PATCH] surete --- surete/04_modeles_synchrones.md | 260 ++++++++++++++++++++++++++++++++ 1 file changed, 260 insertions(+) create mode 100644 surete/04_modeles_synchrones.md diff --git a/surete/04_modeles_synchrones.md b/surete/04_modeles_synchrones.md new file mode 100644 index 0000000..49fc384 --- /dev/null +++ b/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 (: ; ... : ) returns (: ; ... : ) +var : ; : +let + +tel +``` + +Les équations sont des relations entre les paramètres et les valeurs déduites, retournées. + +``` + := 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 +```