24 KiB
Programmation synchrone 2025/2026 – Journal du cours
- Cours 01 <2025-09-29 Mon>
- Cours 02 <2025-10-06 Mon>
- Cours 03 <2025-10-13 Mon>
- Cours 04 <2025-10-20 Mon>
- Cours 05 <2025-10-27 Mon>
- Cours 06 <2025-11-04 Tue>
- Cours 07 <2025-11-10 Mon>
- Cours 08 <2025-11-17 Mon>
- Cours 09 <2025-11-24 Mon>
- Cours 10 <2025-12-01 Mon>
Cours 01 <2025-09-29 Mon>
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.
Cours 02 <2025-10-06 Mon>
On traite des constructions de base du langage.
Cours 03 <2025-10-13 Mon>
On traite des horloges et automates.
Cours 04 <2025-10-20 Mon>
On traite des automates et tableaux.
Cours 05 <2025-10-27 Mon>
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 Tue>
Projet
On traite du fonctionnement du projet.
Cours 07 <2025-11-10 Mon>
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 Mon>
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 Mon>
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.
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.
node counter() returns (o : int)
let
o = 0 -> (pre o + 1);
tel
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.
$ 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.rsL'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.
node top() returns (ok : bool)
var o : int;
let
o = counter();
ok = o >= 0;
--%PROPERTY ok;
tel
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.
$ 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)
====================================================================================================================
(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.
$ time heptc -target c ex0.lus
real 0m0,026s
user 0m0,013s
sys 0m0,013sOn peut montrer des propriétés un peu plus intéressantes, par exemple en écrivant une variante du compteur avec une valeur d'initialisation.
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
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 ?
$ 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
====================================================================================================================
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.
node top(ini : int) returns (ok : bool)
var o : int;
let
o = counterini(ini);
ok = ((ini >= 0) -> true) => (o >= 0);
check ok;
telLa vérification échoue encore, avec le contre-exemple qui suit.
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
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.
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
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.
node top(ini : int) returns (ok : bool)
var o : int;
let
o = counterini(ini);
ok = o >= 0;
check ok provided always((ini >= 0) -> true);
telComparaison 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.
node compare(ini : int) returns (ok : bool)
let
ok = counter() + ini = counterini(ini);
check ok;
tel
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.
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;
telLes 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).
node counterini(ini : int) returns (o : int)
(*@contract
assume (ini >= 0) -> true;
guarantee o >= 0;
*)
let
o = ini -> (pre o + 1);
tel
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.
node counterini(ini : int) returns (o : int)
(*@contract
assume false;
guarantee (o = constant(o));
*)
let
o = ini -> (pre o + 1);
tel
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 Mon>
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
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;
telLes bases de l'algorithmique de la vérification
Les données du problème sont :
- un programme synchrone à vérifier,
- un observateur pour la propriété à démontrer (
check ok), - 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 à 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$.
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 SUCCESSCet 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
KnownetExploredpar votre structure d'ensemble fini favorite, et énumérer les valeurs possibles pour calculerpost(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.
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 SUCCESSLes 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 :
- 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.
- 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.