diff --git a/cours/journal.org b/cours/journal.org index 6020c65..8e6b235 100644 --- a/cours/journal.org +++ b/cours/journal.org @@ -11,25 +11,618 @@ #+LATEX_HEADER: \usepackage[french]{babel} # (org-latex-export-to-pdf) -* Cours 1 <2025-09-29> +* Cours 01 <2025-09-29> On lit le syllabus ainsi que le début des notes. Le manuel d'Heptagon peut être trouvé sur le dépôt git du projet. On peut cliquer sur le bouton /download/ pour télécharger une copie PDF. https://gitlab.inria.fr/synchrone/heptagon/-/blob/ec26be27b91f3e601b98b8b7e15e8d56d4b9afc7/manual/heptagon-manual.pdf -* Cours 2 <2025-10-06> +* Cours 02 <2025-10-06> On traite des constructions de base du langage. -* Cours 3 <2025-10-13> +* Cours 03 <2025-10-13> On traite des horloges et automates. -* Cours 4 <2025-10-20> +* Cours 04 <2025-10-20> On traite des automates et tableaux. -* Cours 5 <2025-10-27> - On traite des tableaux et de la génération d'échantillons audios, disponbile dans son [dossier](audio/). -* Cours 6 <2025-11-04> - On traite du fonctionnement du projet. -* Cours 7 <2025-11-10> - On traite de l'exemple du pendule inversé, disponible dans son [dossier](inverted-pendulum/). - +* Cours 05 <2025-10-27> +** Programmation Heptagon + On traite des tableaux. +** Exemples + On traite la génération d'échantillons audios, disponbile dans son + [dossier](audio/). +* Cours 06 <2025-11-04> +** Projet + On traite du fonctionnement du projet. +* Cours 07 <2025-11-10> +** Exemples + On traite l'exemple du pendule inversé, disponible dans son + [dossier](inverted-pendulum/). +** Implémentation des langages synchrones On commence à expliquer la compilation d'Heptagon, avec l'explication de MiniLS vers Obc jusqu'au traitement des horloges *exclu*. +* Cours 08 <2025-11-17> +** Implémentation des langages synchrones + On discute de la compilation des horloges en MiniLS, de la traduction des + automates et des structures de contrôle plus simples (notamment ~switch~) en + Heptagon. On présente l'analyse d'initialisation. +* Cours 09 <2025-11-24> +** Implémentation des langages synchrones + On termine la partie concernant l'implémentation des langages synchrones. +** Vérification automatique + L'outil Kind2 est un vérificateur de modèle (/model checker/) pour un langage + proche d'Heptagon développé à l'université de l'Iowa. + + https://kind.cs.uiowa.edu + + Un tel outil est une des justifications pour l'emploi d'un langage très + limité comme Heptagon, SCADE et leurs variantes. La vérification automatique + est beaucoup plus difficile lorsque le langage d'entrée est un langage + généraliste comme C, Python ou OCaml. +*** Introduction + Le langage accepté par Kind2 est une variante d'Heptagon beaucoup plus + proche de son ancêtre Lustre. Les différences sont assez mineures mais + peuvent rendre l'écriture du code désagréable lorsqu'on est habitué aux + constructions d'Heptagon. + + Par exemple, le langage ne propose pas l'opérateur ~fby~, uniquement ~pre~ + et ~->~. Notre classique compteur doit donc être écrit comme suit. + + #+BEGIN_SRC +node counter() returns (o : int) +let + o = 0 -> (pre o + 1); +tel + #+END_SRC + + Kind2 est capable de traduire ce programme vers du code impératif, jouant + ainsi le même rôle que le compilateur ~heptc~ pour Heptagon. Plutôt que de + générer du code C, Kind2 produit du code Rust. + + #+BEGIN_SRC +$ kind2 --compile true ex0.lus + kind2 v1.1.0-16-g9572d9b + + System counter has no property, skipping verification step. + +-------------------------------------------------------------------------------- +Post-analysis: rust generation + + Compilation to Rust is still a rather experimental feature: + in particular, arrays are not supported. + + Compiling node "counter" to Rust in `ex0.lus.out/counter/implem`. + + Done compiling. + +-------------------------------------------------------------------------------- +$ wc -l ex0.lus.out/counter/implem/src/main.rs +366 ex0.lus.out/counter/implem/src/main.rs + #+END_SRC + + L'intérêt principal de Kind2 est ailleurs : il est capable de /vérifier + formellement/ des propriétés. Par opposition au test, la vérification + formelle permet de vérifier qu'une propriété est vraie pour *toute* entrée, + plutôt que pour une entrée particulière. De plus, dans le cas des langages + synchrones, les entrées sont des suites infinies, dont on ne peut tester + qu'un préfixe fini. La vérification formelle, elle, considère des entrées de + longueur infinie. + + Lorsqu'on découvre un outil de vérification formelle, un des premières + questions à se poser est celle du langage dans lequel les propriétés sont + écrites. Certains outils de vérification offrent un langage spécialisé pour + ce faire, par exemple une logique temporelle pour le model-checker PRISM. + Les outils de vérification de langages synchrones comme Kind2 font un choix + un peu différent. Le langage des propriétés est le même que celui des + programmes, et la propriété à vérifier est exprimée par un flot booléen + désigné par l'utilisateur doit toujours être vrai. Avec cette approche, on + va avoir tendance à écrire des /observateurs synchrones/, c'est-à-dire des + noeuds qui sont utilisés uniquement pour vérifier que le noeud qui va être + déployé sur le système embarqué final va respecter certaines propriétés, + éventuellement sous certaines hypothèses concernant ses entrées. + + #+BEGIN_SRC +node top() returns (ok : bool) +var o : int; +let + o = counter(); + ok = o >= 0; + --%PROPERTY ok; +tel + #+END_SRC + + En lançant Kind2 sur ce fichier, on lui demande de vérifier que le flot ~ok~ + est toujours vrai. Il est capable de vérifier que c'est le cas, même si ~ok~ + contient une infinité de valeurs. + + #+BEGIN_SRC +$ kind2 ex0.lus + kind2 v1.6.0 + +==================================================================================================================== +Analyzing top + with First top: 'top' + subsystems + | concrete: counter + + Property ok is valid by property directed reachability after 0.148s. + +-------------------------------------------------------------------------------------------------------------------- +Summary of properties: +-------------------------------------------------------------------------------------------------------------------- +ok: valid (at 1) +==================================================================================================================== + #+END_SRC + + (Cet exemple montre que Kind2 suppose que la sémantique du type ~int~ de + Lustre est celle des entiers relatifs, sans limite de taille. Pourquoi ? + Remarquons que jusqu'ici on avait supposé que les types des langages + synchrones étaient tous finis, ce qui assurait la finitude de la mémoire. + Comme on le décrira plus bas, ce choix n'est pas sans conséquences + théoriques et pratiques.) + + Cet exemple laisse aussi deviner que la vérification est un processus + coûteux, beaucoup plus coûteux que la compilation. Ce fichier étant écrit + dans le sous-ensemble commun à Heptagon et Lustre, on peut le compiler avec + ~heptc~ et comparer le temps de compilation au temps de vérification. + + #+BEGIN_SRC +$ time heptc -target c ex0.lus +real 0m0,026s +user 0m0,013s +sys 0m0,013s + #+END_SRC + + On peut montrer des propriétés un peu plus intéressantes, par exemple en + écrivant une variante du compteur avec une valeur d'initialisation. + + #+BEGIN_SRC +node counterini(ini : int) returns (o : int) +let + o = ini -> (pre o + 1); +tel + +node top(ini : int) returns (ok : bool) +var o : int; +let + o = counterini(ini); + ok = o >= 0; + check ok; +tel + #+END_SRC + + Cet exemple est plus intéressant que le précédent en ce que le noeud ~top~ + dispose désormais d'une entrée. Kind2 va donc essayer de vérifier que toutes + les valeurs de la suite ~ok~ sont vraies et ce /pour toutes les suites + d'entrée ~ini~/. Va-t-il réussir ? + + #+BEGIN_SRC shell +$ kind2 ex0.lus + kind2 v1.6.0 + +==================================================================================================================== +Analyzing top + with First top: 'top' + subsystems + | concrete: counterini + + Property ok is invalid by bounded model checking for k=0 after 0.041s. + +Counterexample: + Node top () + == Inputs == + ini -1 + == Outputs == + ok false + == Locals == + o -1 + + Node counterini (top[l14c7]) + == Inputs == + ini -1 + == Outputs == + o -1 + + +-------------------------------------------------------------------------------------------------------------------- +Summary of properties: +-------------------------------------------------------------------------------------------------------------------- +ok: invalid after 0 steps +==================================================================================================================== + #+END_SRC + + La vérification a échoué, mais Kind2 nous a fourni un contre-exemple sous la + forme d'une séquence d'entrées qui falsifie la propriété. Il suffit bien sûr + de donner un ~ini~ strictement négatif au premier instant ! + + Notre propriété est donc fausse. Peut-on exprimer que le flot ~o~ est + toujours vrai mais *à condition* que la première valeur de ~ini~ soit + positive ? Oui, en utilisant l'opérateur booléen d'implication pour exprimer + une /précondition/ (hypothèse) sur l'entrée ~ini~. + + (Remarque : l'implication dont il s'agit ici n'est que l'opérateur + combinatoire sur les flots défini par ~x => y = not x or y~, rien de plus. + En particulier, Kind2 n'a aucun traitement spécifique de cet opérateur.) + + Un premier essai pourrait ressembler à ce qui suit. + + #+BEGIN_SRC +node top(ini : int) returns (ok : bool) +var o : int; +let + o = counterini(ini); + ok = ((ini >= 0) -> true) => (o >= 0); + check ok; +tel + #+END_SRC + + La vérification échoue encore, avec le contre-exemple qui suit. + + #+BEGIN_VERBATIM +Counterexample: + Node top () + == Inputs == + ini -2 0 + == Outputs == + ok true false + == Locals == + o -2 -1 + + Node counterini (top[l19c7]) + == Inputs == + ini -2 0 + == Outputs == + o -2 -1 + #+END_VERBATIM + + Comment comprendre ce contre-exemple ? Au premier instant, ~i~ vaut ~-2~ et + la précondition sur ~ini~ est fausse, donc l'implication est vraie. Au + deuxième instant, la précondition sur ini est vraie, donc l'implication + prend la valeur de ~o >= 0~, qui se trouve fausse. + + Quel est le problème ? Ce que nous avions en tête n'est pas ce que nous + avons écrit. On aurait voulu dire "si ~ini < 0~ au premier instant, la + précondition est fausse pour toujours", mais on a écrit "si ~ini < 0~ au + premier instant, la précondition est fausse /au premier instant/". On peut + régler le problème en introduisant un noeud ~always~ dont la sortie devient + fausse pour toujours dès que son entrée est fausse. + + #+BEGIN_SRC +node always(b : bool) returns (o : bool) +let + o = (true -> pre o) and b; +tel + +node top(ini : int) returns (ok : bool) +var o : int; +let + o = counterini(ini); + ok = always((ini >= 0) -> true) => (o >= 0); + check ok; +tel + #+END_SRC + + La vérification réussit. En particulier, le contre-exemple précédent n'est + plus valide. Si la valeur initiale de ~ini~ est ~-2~, la valeur de + ~always((ini >= 0) -> true)~ sera toujours fausse, et donc la vérité de + l'implication dépendra de ~o >= 0~, toujours vraie. + + Le fait d'exprimer une précondition sur les entrées est très fréquent, et + Kind2 propose une syntaxe un peu plus agréable pour ce faire. + + #+BEGIN_SRC +node top(ini : int) returns (ok : bool) +var o : int; +let + o = counterini(ini); + ok = o >= 0; + check ok provided always((ini >= 0) -> true); +tel + #+END_SRC +*** Comparaison de noeuds + On peut utiliser le principe des observateurs synchrones pour comparer le + comportement de deux noeuds, et éventuellement tester leur équivalence. + + Par exemple, comment quelle relation voyez vous entre notre premier noeud + ~counter~ et le noeud ~counterini~ ? Et comment la feriez-vous vérifier par + Kind2 ? + + Le lien est essentiellement qu'ajouter la première valeur de ~ini~ à la + sortie de ~counter~ donne celle de ~counterini~. La tentative donnée + ci-dessous est trop naïve puisqu'il ne faut prendre en compte ~ini~ + uniquement au premier instant. + + #+BEGIN_SRC +node compare(ini : int) returns (ok : bool) +let + ok = counter() + ini = counterini(ini); + check ok; +tel + #+END_SRC + + On peut utiliser un noeud ~constant~ qui maintient la valeur reçue au + premier instant. On obtient le noeud suivant, dont la propriété est + vérifiée. + + #+BEGIN_SRC +node constant(ini : int) returns (o : bool) +let + o = ini -> pre o; +tel + +node compare(ini : int) returns (ok : bool) +let + ok = counter() + constant(ini) = counterini(ini); + check ok; +tel + #+END_SRC +*** Les contrats + Les propriétés qu'on a vérifié jusqu'ici sont des propriétés globales du + système. Il s'agit certainement d'une approche utile, mais elle n'est pas + tout à fait convaincante du point de vue du génie logiciel. On aimerait + plutôt vérifier chaque noeud indépendamment. Kind2 le permet via l'écriture + de /contrats/ qui permettent à chaque noeud de documenter ses attentes + vis-à-vis de ses appelants (mot-clef /assume/) et ses garanties (mot-clef + /guarantee/). + + #+BEGIN_SRC +node counterini(ini : int) returns (o : int) +(*@contract + assume (ini >= 0) -> true; + guarantee o >= 0; + *) +let + o = ini -> (pre o + 1); +tel + #+END_SRC + + Notez que Kind2 assure la bonne sémantique pour l'hypothèse (/assume/), + c'est-à-dire qu'elle doit être valide de toute la séquence d'entrées, et ce + sans avoir à utiliser une noeud comme ~always~. (Pour ceux et celles d'entre + vous qui connaissent la logique temporelle, si $A$ est la formule booléenne + des hypothèses et $G$ est la formule booléenne des garanties, la formule que + l'outil cherche à démontrer est $\square A \Rightarrow \square G$ plutôt que + $\square A \Rightarrow \square G$. + + Je finis cette partie pratique par une difficulté à laquelle tous les + utilisateurs de vérification formelle finissent par se heurter un jour ou + l'autre : des hypothèses trop fortes rendent la garantie triviale. Voir + ci-dessous pour un exemple caricatural ; /garbage in, garbage out/. + + #+BEGIN_SRC +node counterini(ini : int) returns (o : int) +(*@contract + assume false; + guarantee (o = constant(o)); + *) +let + o = ini -> (pre o + 1); +tel + #+END_SRC + + Cependant, Kind2 aide à détecter le problème. L'outil va chercher à vérifier + que tout appelant à ce ~counterini~ satisfait aux hypothèses, ce qui ici est + impossible... Sauf si l'appelant a lui-même fait des hypothèses + contradictoires sur ses entrées, bien entendu ! +* Cours 10 <2025-12-01> +** Vérification automatique, suite +*** Exemples +**** Compteurs + On va s'intéresser à la vérification d'équivalence entre compteurs + périodiques de 0 à 3, formulé avec des entiers, puis en codage binaire, + classique puis de Gray. + + On commence par écrire le compteur sur deux bits avec un entier + + #+BEGIN_SRC +node intcounter (rst : bool; const max : int) returns (out : bool); +var t : int; +let + t = 0 -> if rst or pre t = max then 0 else pre t + 1; + out = t = 3; +tel + +node graycounter (rst : bool) returns (out : bool); +var a, b : bool; +let + a = false -> (not rst and not pre b); + b = false -> (not rst and pre a); + out = not a and b; +tel + +node bincounter (rst : bool) returns (out : bool); +var a, b : bool; +let + a = false -> (not rst and (pre a <> pre b)); + b = false -> (not rst and not pre b); + out = a and b; +tel + +node top (rst : bool) returns (); +var grayc, binc, intc : bool; +let + grayc = graycounter(rst); + intc = intcounter(rst, 3); + binc = bincounter(rst); + check binc = intc; + check grayc = intc; +tel + #+END_SRC +*** Les bases de l'algorithmique de la vérification + Les données du problème sont : + + 1. un programme synchrone à vérifier, + + 2. un /observateur/ pour la propriété à démontrer (~check ok~), + + 3. un /observateur/ pour l'hypothèse supposée (~assert hyp~). + + L'objectif d'un vérificateur de modèle pour un programme synchrone à flots + de données est de démontrer : + + ~always(so_far(hyp) => ok)~. + + Notons qu'on ne traite que les propriétés de sûreté (``quelque-chose de + mauvais n'arrive toujours'') et pas de vivacité (``quelque-chose de bon + finit toujours par arriver''), comme expliqué au cours précédent. + + On va s'intéresser à ce problème dans le cas *purement booléen*, + c'est-à-dire où toutes les variables manipulées sont des suites de + booléens. Notre description est basée sur le rapport de recherche de Pascal + Raymond disponible à + [[https://www.di.ens.fr/~pouzet/cours/mpri/bib/lesar-rapport.pdf][cette + adresse]]. + + Si $X$ est un ensemble, on écrit $\overline{X}$ pour les fonctions de $X$ + dans $\mathbb{B}$, qui sont en bijection avec les parties de $X$. On + identifiera librement les sous-ensembles et leurs fonctions + charactéristiques dans ce qui suit. + + Les données du problème sont les n-uplets ($V$, $S$, $I \subseteq + \overline{S}$, $g : \overline{S} \times \overline{V} \to \overline{S}$, $H + \subseteq \overline{S} \times \overline{V}$, $\Phi \overline{S} \times + \overline{V}$), où : + + - $S$ et $V$ sont des ensembles *finis* dont les éléments sont + respectivement les variables d'état de d'entrée du programme, + + - $I$ est l'ensemble des états initiaux, + + - $H$ est l'hypothèse, + + - $\Phi$ est la propriété à démontrer. + + On écrira $q \to^v q'$ pour $q' = g(q, v)$ avec $q,q' \in \overline{S}$ et + $v \in \overline{V}$. + + On définit les états successeur/prédécesseurs d'un état $q$ ou d'un + ensemble d'états~$X$ par : + + \begin{align*} + post_H(q) & = \{ q' \mid \exists v \in q \to_v q' \wedge H(q, v) \} + \\ + pre_H(q) & = \{ q' \mid \exists v \in q' \to_v q \wedge H(q', v) \} + \\ + POST_H(X) & = \bigcup_{q \in X} post_H(q) + \\ + PRE_H(X) & = \bigcup_{q \in X} pre_H(q) + \end{align*} + + L'ensemble des états d'erreurs immédiate sont ceux qui satisfont + l'hypothèse mais pas la propriété à démontrer. + + \[ + Err = \{ q \mid \exists v, H(q, v) \wedge \neg \Phi(q, v) \} + \] + + On définit maintenant l'ensemble $Acc$ des états accessibles du programme + et l'ensemble $Bad$ des mauvais états par un plus petit point fixe + ensembliste : $\mu X . F(X)$ désigne le plus petit ensemble $Y$ tel que + $F(Y) \subseteq Y$ ; son existence est garantie dès lors que $F$ est + croissante pour l'inclusion. + + \begin{align*} + Acc & = \mu X. (I \cup POST_H(X)) + \\ + Err & = \{ q \mid \exists v, H(q, v) \wedge \neg \Phi(q, v) \} + \\ + Bad & = \mu X . (Err \cup PRE_H(X)) + \end{align*} + + L'objectif est maintenant de démontrer que le système est *sûr*, + c'est-à-dire que $Acc \cap Bad = \emptyset$. Autrement dit, aucun état + accessible du système n'est un état d'erreur. + + Pour ce faire, il existe deux grandes méthodes : + + - l'exploration en *avant* : on démontre $Acc \cap Err = \emptyset$, + + - l'exploration en *arrière* : on démontre $Bad \cap I = \emptyset$. + + L'approche la plus simple pour ce faire est une approche énumérative : on + explore explicitement l'automate induit par le programme, en imitant le + calcul du plus petit point fixe correspondant à $Acc$ ou $Bad$. + + #+BEGIN_SRC +Known := I; Explored := {} +while there is q in Known \ Explored: + for all q' in post(q): + if q' in Err: + return FAILURE + move q' to Known + move q to Explored +} +return SUCCESS + #+END_SRC + + Cet algorithme peut être implémenté et termine puisque tous les ensembles + manipules sont finis, les prédicats calculables, tout comme la fonction de + transition du programme. En particulier, vous pouvez implémenter les + ensembles ~Known~ et ~Explored~ par votre structure d'ensemble fini + favorite, et énumérer les valeurs possibles pour calculer ~post(q)~. Il + s'agit donc en somme d'exécuter le programme sur toutes les entrées + possibles ; on voit que c'est très inefficace. + + On peut aussi implémenter une version en arrière. + + #+BEGIN_SRC +Known := Err; Explored := {} +while there is q in Known \ Explored: + for all q' in pre(q): + if q' in I: + return FAILURE + move q' to Known + move q to Explored +} +return SUCCESS + #+END_SRC + + Les deux algorithmes sont très inefficaces, tellement qu'ils en deviennent + inutilisables en pratique. En effet, les structures de données + représentant les ensembles d'état ou d'entrées deviendront très grosses, + et les calculs attenants (différence ensembliste, ajout, choix d'un + élément...) coûteux à réaliser. + + Notons que le second algorithme est encore moins efficace que le + premier. Voyez-vous pourquoi ? Le calcul de ~pre(q)~ est encore plus + coûteux, puisqu'il faut calculer l'image inverse de la fonction de + transition $g$, c'est-à-dire trouver l'ensemble des $q'$ tel que $g(q', v) + = q$ pour $v$ et $q$ fixés. + + Depuis les années 1990, on utilise plutôt des méthodes dites + *symboliques*. L'idée générale est de représenter les ensembles finis par + des formules logiques plutôt que par des énumérations explicites. Par + exemple, on pourrait représenter l'ensemble $\{ (x, y, z) \mid x + \overline{y} + z = 1 \}$ directement par le *code* de sa fonction + caractéristique $f(x, y, z) = x \overline{y} + z$ plutôt qu'explicitement + par l'ensemble de triplets $\{ (1, 0, 0), (1, 0, 1), (0, 0, 1), (0, 1, 1), + (1, 1, 1) \}$. Les méthodes symboliques sont donc un exemple de compromis + temps-espace : on y gagne une représentation nettement plus succincte des + données que la représentation explicite, en contrepartie de quoi les + opérations (notamment test d'égalité, du vide, d'inclusion, etc.) seront + plus coûteuses. + + Il existe deux grandes méthodes d'implémentation pour exprimer les + opérations et les tests : + + 1. On peut représenter les formules directement par leur code et utiliser + un solveur SAT général pour répondre aux questions intéressantes pour + la vérification. Par exemple, l'ensemble $\{ \vec{x} \mid \phi(\vec{x}) + \}$ est inclus dans l'ensemble $\{ vec{x} \mid \psi(\vec{x}) \}$ si et + seulement si $\forall \vec{x}, \phi(\vec{x}) \implies \psi(\vec{x})$, + question à laquelle un solveur SAT peut répondre, y compris pour de + très grosses formules $\phi$ et $\psi$. D'autres questions, comme par + exemple l'énumération des valeurs appartenant à un ensemble, sont d'un + traitement moins direct mais peuvent être gérée avec un peu de + réflexion et d'effort. + + 2. On peut utiliser une représentation canonique des formules booléennes, + par exemple les /diagrammes de décision binaire/ (ou /binary decision + diagrams/ en anglais, BDD). Ici, toutes les formules équivalentes sont + représentées par la même structure de données. La construction de cette + représentation est donc forcément coûteuse, mais une fois construite on + peut l'utiliser pour répondre efficaement à beaucoup de questions. C'est + cette approche qui est très bien exposée dans le rapport de P. Raymond + cité plus haut. + + Le principe des diagrammes de décision binaire a été brièvement expliqué en + cours mais ne sera pas détaillé dans ces notes.