367 lines
12 KiB
Markdown
367 lines
12 KiB
Markdown
---
|
||
title: "Conception formelle : Validation et vérification"
|
||
date: 2023-01-13
|
||
tags: ["Bugs", "model-checking"]
|
||
categories: ["Conception formelle", "Cours"]
|
||
mathjax: true
|
||
---
|
||
|
||
## Définition
|
||
|
||
### Validation
|
||
|
||
Losqu'un modèle ressemble à un système, alors il devient alors un candidat pour
|
||
devenir un système réel. Mais alors **comment décider qu'un modèle est valide**?
|
||
|
||
Il doit satisfaire toutes des propriétés qui définissent un bon candidat, mais
|
||
une liste de telles propriétés n'existe pas. Uen liste minimale de propriétés
|
||
dépends avant tout du type d'application. Pour la validation, les outils de
|
||
simulation (jouer des scénario pour observer) sont consiérés comme adaptés.
|
||
|
||
la Validation permet donc de s'assurer **d'avoir construit quelque chose
|
||
d'adapté**
|
||
|
||
### Vérification
|
||
|
||
Le modèle doit vérifier tous les pré-requis décrits dans les spécifications.
|
||
Nous vérifions alors que le modèle satisfasse toutes les exigences du cahier des
|
||
charges.
|
||
|
||
Ici la simulation n'est pas considérée comme une technique adaptée. Par contre
|
||
la vérification de modèle (*model checking*) est un bon moyen de vérification.
|
||
|
||
## Model Checking
|
||
|
||
\\(
|
||
\begin{array}{l}
|
||
{Model\ M} \to \\\
|
||
{Spec\ \varphi} \to \\\
|
||
\end{array}
|
||
\boxed{
|
||
\begin{array}{l}
|
||
{Model} \\\
|
||
{Checking} \\\
|
||
\end{array}
|
||
}
|
||
\to \? M \models \varphi
|
||
\\)
|
||
|
||
En entrée nous avons notre modèle \\(M\\) et notre spécification \\(\varphi\\),
|
||
nous devons alors vérifier que \\(M\\) modélise \\(\varphi\\).
|
||
|
||
### Deux classes de propriété
|
||
|
||
#### Sureté
|
||
|
||
Quelque chose **est impossible**, une configuration est inaccessible par
|
||
exemple. À la suite d'un événement, un autre ne peut être atteint. Si une
|
||
propriété de sureté est non-satisfaite, alors le contre exemple est un scénario
|
||
fini.
|
||
|
||
**Il faut s'assurer que quelque chose de mauvais n'arrive jamais**
|
||
|
||
#### Vivacité
|
||
|
||
À l'inverse de la sureté, quelque chose est **toujours possible**. Un événement
|
||
est toujours suivi d'un autre événement dans un temps fini. Quoi que l'on fasse,
|
||
on arrive toujours à *B* après *A*. Si une propriété de vivacité est non
|
||
satisfaire, alors le contre exemple est un scénario infini.
|
||
|
||
**Il faut s'assurer que quelque chose de bien arrive toujours**
|
||
|
||
### Limites théoriques
|
||
|
||
Il existe deux grande famille de classe de couples modèles / spécification :
|
||
|
||
* **systèmes finis**: toutes les formules, d'un point de vue logique sont
|
||
décidable (calculable), il existe d'ailleurs un ensemble d'outils académiques
|
||
pour le faire.
|
||
* **systèmes infinis**: seules quelques formules sont décidable (automates avec
|
||
des compteurs, des horloges, des file FIFO). Il n'existe que quelques
|
||
documents de recherches et peut d'outils
|
||
|
||
### Limites pratiques
|
||
|
||
La première de ces limites concerne le matériel (CPU, RAM, etc.). La
|
||
représentation de certains graphes peut être relativement gourmande
|
||
|
||
La seconde concerne les limites logiques. Modéliser est une tâche complexe, des
|
||
difficultés peuvent apparaître notamment lorsqu'il s'agit de s'assurer qu'un
|
||
modèle est valide.
|
||
|
||
## Formalisme
|
||
|
||
D'après [Wikipedia][l_formalisme]: Un formalisme a pour objectif de représenter
|
||
de manière non-ambiguë un objet d'étude en science
|
||
|
||
[l_formalisme]:https://fr.wikipedia.org/wiki/Formalisme
|
||
|
||
### Outils
|
||
|
||
Nous avons à notre disposition tout un tas d'outils pour décrire les
|
||
formalismes:
|
||
|
||
* Réseaux de Petri
|
||
* State Charts
|
||
* Message Sequence Chart (diagrammes de séquence en UML)
|
||
* Diagrammes de flux très utilisés par les électroniciens
|
||
* Process Algebra
|
||
* Les langages dédiés
|
||
|
||
### Choix de la logique
|
||
|
||
* CTL -- *Computational Tree Logic*
|
||
* LTL -- *Linear Tree Logic*
|
||
* Hennessy-Milner Logic
|
||
* Calcul infinitésimal
|
||
* La logique de Dicky, logique basée sur les états.
|
||
|
||
### Pour ce cours
|
||
|
||
Nous nous limiterons aux variables avec un domaine fini: exit donc les `int`,
|
||
`float`, `string` etc. Nous utiliserons les **intervales** et les
|
||
**énumérations** (`enum`).
|
||
|
||
Comme outil, nous utiliserons *Altarica Checker* qui utilise la logique de Dicky
|
||
et u-calculus. Le tout avec des relation dans des domaines finis.
|
||
|
||
## La logique de Dicky
|
||
|
||
Soit le graphe suivant:
|
||
|
||
|
||
|
||
D'après le graphe, trouvons les états:
|
||
|
||
* `a` est-il possible?: \\(\\{(0,a,1), (5,a,6), (2,a,5)\\}\\)
|
||
* `c` est-il possible?: \\(\\{(2,c,3), (4,c,5)\\}\\)
|
||
* avant `a`: \\(\\{0,5,2\\}\\)
|
||
* après `c`: \\(3,5\\)
|
||
* `c.a` possible?: \\((avant\ a) \cup (après\ c) = \\{5\\}\\)
|
||
|
||
|
||
Il est question de logique comportementale : on s'intéresse au comportement
|
||
d'un système. Une propriété logique est un ensemble de conditions, dans notre
|
||
exemple la preuve que `c.a` est possible. Comment vérifier, calculer ces
|
||
propriétés? Par un **algorithme de parcours de graphes** avec une complexité
|
||
linéaire.
|
||
|
||
Nous utilisons aussi la logique ensemblistes (union, intersection etc.).
|
||
|
||
Nous avons dans les graphes deux type de propriétés : les **états** et les
|
||
**transitions**.
|
||
|
||
### Les constantes
|
||
|
||
Pour chaque automate, nous avons des constantes de disponibles. Commençons par
|
||
les constantes vides :
|
||
|
||
* `empty_s`: état vide
|
||
* `empty_t`: transition vide
|
||
|
||
Nous avons ensuite les *sets de **tout*** :
|
||
|
||
* `any_s`: tous les états
|
||
* `any_t`: toutes les transitions
|
||
|
||
Les sets d'états initiaux: `initial`
|
||
|
||
Et un ensemble de transitions `self`, `epsilon`, `self-epsilon` : boucles sur
|
||
les états.
|
||
|
||
Il est possible de calculer des expressions élémentaires via des variables, par
|
||
exemple \\([ s \\% 2 = 0 ]\\).
|
||
|
||
Permet de trouver les états pairs.
|
||
|
||
### Les calculs
|
||
|
||
Il est possible de calculer des sets d'états et de transitions.
|
||
|
||
Les sets d'états : \\([expr]\\) où `expr` est un expression, par exemple
|
||
`[light.on]` donne les états ou la lumière est allumée.
|
||
|
||
Les sets de transitions \\(\text{label expr}\\) où `expr` est une expression, par
|
||
exemple `label button.push` donne les transitons qui porte sur l'évènement
|
||
`push`.
|
||
|
||
### Opérateurs ensemblistes
|
||
|
||
Il est possible d'utiliser des opérateurs ensemblistes comme l'union et
|
||
l'intersection
|
||
|
||
Soit \\(F_1\\) et \\(F_2\\) deux formules du même type:
|
||
|
||
\\(
|
||
[\\![ F_1 \text{ et } F_2 ]\\!] = [\\![ F_1 \\&\\& F_2 ]\\!] = [\\![ F_1 \cap F_2 ]\\!]
|
||
\\\
|
||
[\\![ F_1 \text{ ou } F_2 ]\\!] = [\\![ F_1 \\| F_2 ]\\!] = [\\![ F_1 \cup F_2 ]\\!]
|
||
\\)
|
||
|
||
Soit \\(S\\) une formule d'états et \\(T\\) une formule de transitions :
|
||
|
||
\\(
|
||
[\\![not S]\\!] = [\\![any_s]\\!] \setminus [\\![S]\\!]
|
||
\\\
|
||
[\\![not T]\\!] = [\\![any_t]\\!] \setminus [\\![T]\\!]
|
||
\\)
|
||
|
||
ici \\(\setminus\\) représente une différence ensembliste.
|
||
|
||
### Opérateur source, destination
|
||
|
||
Soit \\(T\\) une formule de transitions
|
||
|
||
* \\(\text{src}(T)\\) représente l'ensemble **des états source** d'au moins une
|
||
transition de \\(T\\)
|
||
* \\(\text{tgt}(T)\\) représente l'ensemble **des états destination** d'au
|
||
moins une transition de \\(T\\)
|
||
|
||
Soit \\(S\\) une formule d'état
|
||
|
||
* \\(\text{rsrc}(S)\\) représente les **transitions qui ont leurs source** dans
|
||
au moins un état de \\(S\\)
|
||
* \\(\text{rtgt}(S)\\) représente les **transitions qui ont leurs destination**
|
||
dans au moins un état de \\(S\\)
|
||
|
||
#### Exemples
|
||
|
||
\\(\text{any_s} - \text{src}(\text{any_t})\\) rerésente les états qui sont
|
||
source d'aucune transition, dont on ne peut pas sortir (état puit)
|
||
|
||
\\(\text{src}(\text{rtgt}(S) \cap T)\\) représente les états utilisant les
|
||
transitions \\(T\\) pour mener à \\(S\\).
|
||
|
||
### Reach, coreach et loop
|
||
|
||
Ces opérateurs permettent de calculer des formules, dans les explications
|
||
suivantes \\(S\\) est une formule d'état et \\(T, T_1, T_2\\) des formules de
|
||
transitions:
|
||
|
||
* \\(\text{reach}(S,T)\\) représente tous les états au départ de \\(S\\) avec
|
||
\\(T\\) comme transitions
|
||
* \\(\text{coreach}(S,T)\\) représente tous les états avec comme destination
|
||
\\(S\\) et utilisants \\(T\\) comme transitions.
|
||
* \\(\text{loop}(T_1,T_2)\\) calcule des transitions, elle représente les
|
||
*Strongly Connected Components* (SCC). C'est une formule de transition tel
|
||
que \\(T_3 \subseteq T_2\\) et \\(T_3 \cap T_1 \neq \emptyset\\). Ces *SCC*
|
||
déterminent toutes situations permettant de revenir à la situation initiale.
|
||
|
||
## ARC
|
||
|
||
*ARC* est le *model checker* d'Altarica, c'est un interpréteur de commande.
|
||
|
||
### Les propriétés
|
||
|
||
En plus des propriétés heritées de la logique de *Dicky*, il existe dans ARC les
|
||
propriété calculées suivantes pour chaque nœud:
|
||
|
||
* `epsilon` : ensemble de transitons etiquetées \((\epsilon\\).
|
||
* `self` : transitions dont la source est la destination sont égaux
|
||
* `self-epsilon`L définis par \\(epsilon \cap \text{self} \\)
|
||
* `not_deterministic`: ensemble de transition non déterministe definies plus
|
||
formellement par
|
||
\\(\\{(s,e,t_1) \in E | \exists t_2 /in V, (s,e,t_2) \in E\\}\\)
|
||
|
||
#### Exemple
|
||
|
||
```
|
||
with Switch, CircuitV1, Scheduler do
|
||
// deadlock: états puit
|
||
deadlock := any_s - src(any_t - self_epsilon);
|
||
|
||
// notResetable : on ne peut pas revenir à l'état initial
|
||
notResettable := any_t - coreach(initial, any_t);
|
||
done
|
||
|
||
with CircuitV1, CircuitV2, CircuitV1_OK do
|
||
bug := any_s & [L.on & ~L.ok];
|
||
action := any_t & (label S.push | label G.failure | label G.repair);
|
||
reaction := any_t & ((label L.reaction | epsilon) − self_epsilon);
|
||
|
||
CFC_reaction := rsrc(reach(any_s & tgt(reaction),reaction)
|
||
& coreach(any_s & src(reaction),reaction)) & rtgt(reach(any_s
|
||
& tgt(reaction),reaction)
|
||
& coreach(any_s & src(reaction),reaction))
|
||
& reaction;
|
||
done
|
||
|
||
with SchedulerRandom, SchedulerPriority, Scheduler do
|
||
bug := (label PJ[1].get & rsrc([PJ[0].nbJobs>0]))
|
||
| (label PJ[2].get & rsrc([PJ[0].nbJobs>0
|
||
| PJ[1].nbJobs>0]));
|
||
done
|
||
```
|
||
|
||
### Les opérateurs
|
||
|
||
En plus des oérateurs disponibles dnas la logique de Dicky, ARC implémente les
|
||
opérateurs suivants:
|
||
|
||
* \\(trace(S_1, T, S_2)\\) : ensemble de transitions représentant le chemin le
|
||
plus court de \\(S_1\\) vers \\(S_2\\) en utilisant les transitions\\(T\\).
|
||
* \\(project(S,T, 'newNodeName', boolean, aNode)\\) : construit une nouveau
|
||
nœud AltaRica avec toutes les transitions \\(T\\) prenant leurs origines dans
|
||
\\(S\\) en restectant les déclarations de \\(aNode\\) (cette déclaration est
|
||
facultative).
|
||
|
||
`trace` nous sera utile pour trouver des contre-exemple et `project` pour
|
||
calculer des contrôleurs pour notre système.
|
||
|
||
|
||
Voici un exemple de commandes `ARC`:
|
||
|
||
```
|
||
with Switch, CircuitV1, Scheduler do
|
||
show(all) > ’$NODENAME.prop’;
|
||
test(deadlock,0) > ’$NODENAME.res’;
|
||
test(notResettable,0) >> ’$NODENAME.res’;
|
||
done
|
||
|
||
with CircuitV1, CircuitV2, CircuitV1_OK do
|
||
quot() > ’$NODENAME.dot’;
|
||
tr_CFC_reaction := trace(initial,any_t,src(CFC_reaction));
|
||
ce_CFC_reaction := reach(src(tr_CFC_reaction), tr_CFC_reaction
|
||
| CFC_reaction);
|
||
dot(ce_CFC_reaction, tr_CFC_reaction|CFC_reaction) > ’$NODENAME−CFC_reaction.dot’;
|
||
show(tr_CFC_reaction, ce_CFC_reaction) >> ’$NODENAME.prop’;
|
||
done
|
||
```
|
||
Ce qui donnera en sortie :
|
||
|
||
```
|
||
TEST(deadlock, 0) [PASSED]
|
||
TEST(notResettable, 0)
|
||
[FAILED] (!= 6)
|
||
TEST(syst_instable, 0)
|
||
[FAILED] (!= 4)
|
||
```
|
||
|
||
### Methodologie
|
||
|
||
nous allons utiliser cet outils comme un **déboggeur de modèle**, en respectant
|
||
les étapes suivantes:
|
||
|
||
1. identifier les composants de base
|
||
2. choisir entre le design *fonctionnel* ou *architectural* en fonction de
|
||
l'objectif et de ce que l'on sait faire.
|
||
3. choisir entreun système **ouvert** ou **fermé** (restreindre le système a
|
||
des cas d'utilisation)
|
||
4. construire l'arborescence du bas vers le haut
|
||
|
||
### Validation d'un premier modèle
|
||
|
||
1. validation de la topologie du graphe (*SCC*, *deadlock*)
|
||
2. propriété dépendantes de l'application (pas de réaction infinie)
|
||
3. toues les évèmements sont utiles
|
||
4. visualisation de petits composants
|
||
5. simutation
|
||
|
||
les étapes 1 et 2 sont à répéter jusqu'à obtention d'un modèle valide.
|
||
|
||
### Vérification du modèle
|
||
|
||
Les spécification son écrites comme une liste de propiété logique et utilise la
|
||
logique de *Dicky* enrichie des éléments vu dans cette partie. Pour chacune des
|
||
propriétés ne satifaisant pas le modèle, **un contre exemple le plus petit
|
||
possible doit être calculé**.
|