Programmation synchrone 2022/2023 – Journal du cours

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. Son intérêt est néanmoins ailleurs : il est capable de vérifier des propriétés.

Certains outils demandent d'utiliser un langage spécialisé pour exprimer les propriétés, 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 valeur ; intuitivement, la décidabilité du problème est conséquence du caractère fini de la mémoire de tout programme synchrone.

$ 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.041s.

--------------------------------------------------------------------------------------------------------------------
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 ?)

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.

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;
  --%PROPERTY 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ée 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 '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);
  --%PROPERTY ok;
tel

La vérification échoue encore, avec le contre-exemple qui suit.

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);
  --%PROPERTY ok;
tel

La vérification réussie. 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 l'implication toujours vraie.

Le fait d'exprimer une précondition sur les entrées en utilisant des noeuds comme always est suffisamment fréquent pour que Kind2 propose un support dédié.

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 ?

Une solution est le noeud suivant, qui vérifie qu'ajouter la première valeur de ini au noeud counter() donne le même résultat que inicounter(ini).

node compare(ini : int) returns (ok : bool)
var ini0 : int;
let
  ini0 = ini -> pre ini0;
  ok = counter() + ini0 = counterini(ini);
  --%PROPERTY ok;
tel

On se ramène à un problème logique en traduisant un noeud Lustre en un système de transition à état fini. Il s'agit d'un système décrit par des formules de logique propositionnelle, et les algorithmes de vérification utilisent donc des solveurs SAT et SMT.

Rappels de logique élémentaire : une valuation \(s\) est une fonction des variables propositionnelles dans les booléens. Une valuation \(s\) satisfait une formule \(F\), ce qu'on note \(s \models F\), lorsque la formule obtenue en remplaçant toute variable \(x\) dans \(F\) par \(s(x)\) est vraie. On écrit \(F \Rightarrow G\) lorsque toute valuation satisfaite par \(F\) est satisfaite par \(G\).

Dans ce qui suit, on suppose que pour chaque variable propositionnelle \(x\) on dispose d'une variable propositionnelle choisie \(x'\) distincte de tous les autres \(y\) et \(y'\). Si \(F\) est une formule, \(F'\) désigne la même formule où toute variable \(x\) a été substituée par \(x'\).

Un système de transition à état fini est un triplet \(S = (\overline{x}, I, T)\) où \(\overline{x}\) est une liste de variables propositionnelles appelée variables d'état, \(I\) une formule logique dont les variables libres appartiennent à \(\overline{x}\) appelée états initiaux, et \(T\) une formule logique sur les variables \(\overline{x}\) et les variables \(\overline{x}'\) appelée relation de transition.

Un état \(s\) est une valuation de \(\overline{x}\).

Une trajectoire est une suite d'états \(s_0,s_1,\dotsc\) telle que \(s_0 \models I\) satisfait \(I\) et \(s_i, s_{i+1}' \models T\). Autrement dit, c'est une suite d'états telle que le premier est initial et chaque paire d'états consécutifs de la suite appartient à la relation de transition.

Un état qui apparaît dans une trajecotire est dit atteignable.

Le problème de vérification de modèle correspond à la donnée d'une propriété \(P\), définie comme un prédicat sur \(\overline{x}\), et donc un ensemble d'états. Le but d'un vérificateur va être de prouver que tout état \(s\) atteignable est tel que \(s \models P\).

(Dans le cas de Kind2, les propriétés \(P\) vont décrire exactement l'ensemble des états où ok vaut true.)

La stratégie générale pour démontrer que \(P\) est un invariant est toujours la même : on cherche une formule \(F\) qui satisfait les trois propriétés suivantes.

1. \(I \Rightarrow F\)
2. \(F \wedge T \Rightarrow F'\)
3. \(F \Rightarrow P\).

On dit qu'une formule \(F\) qui satisfait les deux premières propriétés est inductive.