153 lines
4.9 KiB
Markdown
153 lines
4.9 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**.
|