diff --git a/content/conception_formelle/2_verification/index.md b/content/conception_formelle/2_verification/index.md index a5654d6..d3948ba 100644 --- a/content/conception_formelle/2_verification/index.md +++ b/content/conception_formelle/2_verification/index.md @@ -16,14 +16,14 @@ devenir un système réel. Mais alors **comment décider qu'un modèle est valid 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. +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. +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. @@ -47,17 +47,16 @@ la vérification de modèle (*model checking*) est un bon moyen de vérification \\) En entrée nous avons notre modèle \\(M\\) et notre spécification \\(\varphi\\), -nous devons alors vérifier que \\(M\\) modélise \\(\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. +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** @@ -142,7 +141,7 @@ D'après le graphe, trouvons les états: 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 +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. @@ -171,12 +170,21 @@ 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 ]\\) +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 @@ -184,47 +192,57 @@ 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 + * \\(\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\\) + * \\(\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 + * \\(\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 +#### 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**) +\\(\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 formulesde +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 destnation + * \\(\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 transition, elle représente les + * \\(\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. @@ -238,9 +256,9 @@ transitions: 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` : + * `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 self \\) + * `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\\}\\) @@ -249,24 +267,39 @@ propriété calculées suivantes pour chaque nœud: ``` with Switch, CircuitV1, Scheduler do + // deadlock: états puit deadlock := any_s - src(any_t - self_epsilon); - notSCC := any_t - loop(any_t, any_t); + + // notResetable : on ne peut pas revenir à l'état initial + notResettable := any_t - coreach(initial, any_t); done + with CircuitV1, CircuitV2, CircuitV1_OK do - bug := [L.on & ~L.ok]; - notControl := (label G.failure | label L.reaction | epsilon) - self_epsilon; + 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); - // IR means infinite reactions - IR := loop(notControl, notControl); + 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 long de \\(S_1\\) vers \\(S_2\\) en utilisant les transitions\\(T\\). + 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 @@ -275,9 +308,38 @@ opérateurs suivants: `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 ocmme un **déboggeur de modèle**, en respectant +nous allons utiliser cet outils comme un **déboggeur de modèle**, en respectant les étapes suivantes: 1. identifier les composants de base @@ -295,7 +357,7 @@ les étapes suivantes: 4. visualisation de petits composants 5. simutation -les étapes 1 et deux sont à répéter jusqu'à obtention d'un modèle valide. +les étapes 1 et 2 sont à répéter jusqu'à obtention d'un modèle valide. ### Vérification du modèle