From e4563cd8797b5e148a13d9e47efd6f3efdb48d61 Mon Sep 17 00:00:00 2001 From: Yorick Barbanneau Date: Wed, 1 Feb 2023 00:48:48 +0100 Subject: [PATCH] Add first part of verification lecture --- .../2_verification/images/dickys.svg | 616 ++++++++++++++++++ .../2_verification/index.md | 153 +++++ 2 files changed, 769 insertions(+) create mode 100644 content/conception_formelle/2_verification/images/dickys.svg create mode 100644 content/conception_formelle/2_verification/index.md diff --git a/content/conception_formelle/2_verification/images/dickys.svg b/content/conception_formelle/2_verification/images/dickys.svg new file mode 100644 index 0000000..58c02c3 --- /dev/null +++ b/content/conception_formelle/2_verification/images/dickys.svg @@ -0,0 +1,616 @@ + + + + + + Interception + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Interception + + + Yorick Barbanneau ^ ephase + + + + + CC BY-SA + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/content/conception_formelle/2_verification/index.md b/content/conception_formelle/2_verification/index.md new file mode 100644 index 0000000..3550284 --- /dev/null +++ b/content/conception_formelle/2_verification/index.md @@ -0,0 +1,153 @@ +--- +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: + +![Graphe ](./images/dickys.svg) + +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**.