--- 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**. ### 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 calcules 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)\\) 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\\)