ephase/cours
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Some corrections.

Browse source
This commit is contained in:
Yorick Barbanneau 2023-09-01 22:18:00 +02:00
parent 9a020327b3
commit 873a41f73a
1 changed files with 96 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

130
content/conception_formelle/2_verification/index.md
View file

@ -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 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 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 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 la Validation permet donc de s'assurer **d'avoir construit quelque chose
d'adapté** d'adapté**
### Vérification ### 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 Nous vérifions alors que le modèle satisfasse toutes les exigences du cahier des
charges. 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\\), 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é ### Deux classes de propriété
#### Sureté #### Sureté
Quelque chose **est impossible**, une configuration est inaccessible par Quelque chose **est impossible**, une configuration est inaccessible par
exemple. À la suite d'un événement, un autre ne peut être atteint. 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
Si une propriété de sureté est non-satisfaite, alors le contre exemple est un fini.
scénario fini.
**Il faut s'assurer que quelque chose de mauvais n'arrive jamais** **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 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 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é propriétés? Par un **algorithme de parcours de graphes** avec une complexité
linéaire. linéaire.
@ -171,12 +170,21 @@ Et un ensemble de transitions `self`, `epsilon`, `self-epsilon` : boucles sur
les états. les états.
Il est possible de calculer des expressions élémentaires via des variables, par Il est possible de calculer des expressions élémentaires via des variables, par
exemple: exemple \\([ s \\% 2 = 0 ]\\).
\\([ s \\% 2 = 0 ]\\)
Permet de trouver les états pairs. 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 ### Opérateurs ensemblistes
Il est possible d'utiliser des opérateurs ensemblistes comme l'union et 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: 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{ 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 ]\\!] [\\![ 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 ### Opérateur source, destination
Soit \\(T\\) une formule de transitions 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\\) transition de \\(T\\)
* \\(\text{tgt}(T)\\) représente l'ensemble des états destination d'au moins * \\(\text{tgt}(T)\\) représente l'ensemble **des états destination** d'au
une transition de \\(T\\) moins une transition de \\(T\\)
Soit \\(S\\) une formule d'état Soit \\(S\\) une formule d'état
* \\(\text{rsrc}(S)\\) représente les transitions qui ont leurs source dans au * \\(\text{rsrc}(S)\\) représente les **transitions qui ont leurs source** dans
moins un état de \\(S\\) au moins un état de \\(S\\)
* \\(\text{rtgt}(S)\\) représente les transitions qui ont leurs destination * \\(\text{rtgt}(S)\\) représente les **transitions qui ont leurs destination**
dans au moins un état de \\(S\\) dans au moins un état de \\(S\\)
### Exemples #### Exemples
\\(\text{any_s} - \text{src}(\text{any_t})\\) rerésente les états qui sont \\(\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) 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 \\(\text{src}(\text{rtgt}(S) \cap T)\\) représente les états utilisant les
transitions vers \\(D\\) (**à vérifier**) transitions \\(T\\) pour mener à \\(S\\).
### Reach, coreach et loop ### Reach, coreach et loop
Ces opérateurs permettent de calculer des formules, dans les explications 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: transitions:
* \\(\text{reach}(S,T)\\) représente tous les états au départ de \\(S\\) avec * \\(\text{reach}(S,T)\\) représente tous les états au départ de \\(S\\) avec
\\(T\\) comme transitions \\(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. \\(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 *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* 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. 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 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: 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` : 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 * `not_deterministic`: ensemble de transition non déterministe definies plus
formellement par formellement par
\\(\\{(s,e,t_1) \in E | \exists t_2 /in V, (s,e,t_2) \in E\\}\\) \\(\\{(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 with Switch, CircuitV1, Scheduler do
// deadlock: états puit
deadlock := any_s - src(any_t - self_epsilon); 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 done
with CircuitV1, CircuitV2, CircuitV1_OK do with CircuitV1, CircuitV2, CircuitV1_OK do
bug := [L.on & ~L.ok]; bug := any_s & [L.on & ~L.ok];
notControl := (label G.failure | label L.reaction | epsilon) - self_epsilon; 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 CFC_reaction := rsrc(reach(any_s & tgt(reaction),reaction)
IR := loop(notControl, notControl); & 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 done
``` ```
### Les opérateurs ### Les opérateurs
En plus des oérateurs disponibles dnas la logique de Dicky, ARC implémente les En plus des oérateurs disponibles dnas la logique de Dicky, ARC implémente les
opérateurs suivants: opérateurs suivants:
* \\(trace(S_1, T, S_2)\\) : ensemble de transitions représentant le chemin le * \\(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 * \\(project(S,T, 'newNodeName', boolean, aNode)\\) : construit une nouveau
nœud AltaRica avec toutes les transitions \\(T\\) prenant leurs origines dans nœud AltaRica avec toutes les transitions \\(T\\) prenant leurs origines dans
\\(S\\) en restectant les déclarations de \\(aNode\\) (cette déclaration est \\(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 `trace` nous sera utile pour trouver des contre-exemple et `project` pour
calculer des contrôleurs pour notre système. 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 ### 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: les étapes suivantes:
1. identifier les composants de base 1. identifier les composants de base
@ -295,7 +357,7 @@ les étapes suivantes:
4. visualisation de petits composants 4. visualisation de petits composants
5. simutation 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 ### Vérification du modèle