captain/progsync
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

journal cours 9

Browse Source
This commit is contained in:
Adrien Guatto
2025-12-01 16:07:58 +01:00
parent 6c8abfbade
commit e8e6d683d4
1 changed files with 604 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

613
cours/journal.org
View File

@@ -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>
* 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 7 <2025-11-10>
On traite de l'exemple du pendule inversé, disponible dans son [dossier](inverted-pendulum/).
* 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
<Note> System counter has no property, skipping verification step.
--------------------------------------------------------------------------------
Post-analysis: rust generation
<Note> 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
<Success> 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
<Failure> 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.