305 lines
10 KiB
Markdown
305 lines
10 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 (jper 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.
|
|
|
|
### 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 ]\\!]
|
|
\\)
|
|
|
|
### 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 sources de
|
|
transitions vers \\(D\\) (**à vérifier**)
|
|
|
|
### 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 formulesde
|
|
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 destnation
|
|
\\(S\\) et utilisants \\(T\\) comme transitions.
|
|
* \\(\text{loop}(T_1,T_2)\\) calcule des transition, 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` :
|
|
* `self` : transitions dont la source est la destination sont égaux
|
|
* `self-epsilon`L définis par \\(epsilon \cap 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 := any_s - src(any_t - self_epsilon);
|
|
notSCC := any_t - loop(any_t, any_t);
|
|
done
|
|
with CircuitV1, CircuitV2, CircuitV1_OK do
|
|
bug := [L.on & ~L.ok];
|
|
notControl := (label G.failure | label L.reaction | epsilon) - self_epsilon;
|
|
|
|
// IR means infinite reactions
|
|
IR := loop(notControl, notControl);
|
|
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 long 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.
|
|
|
|
### Methodologie
|
|
|
|
nous allons utiliser cet outils ocmme 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 deux 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é**.
|