Lien de la note Hackmd
Si on a un ping pong, comment on verifie que l’algo marche ?
On lance et un espere que ca marche? Non ca c’est etre religieux
Il faut check toutes les relations et entralecements possibles (effets de bord, etc).
Il faut faire des preuves automatiques
On va prendre des outils capables d’en faire, en utilisant
- La description $\neq$ implementation du systeme distribue
- S’abstraire des pbs de langage
Qu’est-ce qu’un systeme ?
On veut qu’une fusee n’explose pas en vol
Why is a model required ?
On va considerer que TOUS les systemes qu’on etudie soit un systeme infini.
Le code suivant serveur peut etre considere un systeme:
unsigned received_= 0;
while (1)
{
accept_request();
received_ = received_ + 1 ;
reply_request();
}
Avec un modele, on enleve le probleme de received_
A more realistic example
On a une abstraction des differents comportements de notre systeme
On est capable de construire l’integralite du systeme. On veut faire le produit cartesien de tout le monde.
A l’etat initial du systeme, tout le monde est dans l’etat $1$.
Pour passer de l’etat $111$ a l’etat $211$, on doit avoir en meme temps un message recu et en transit.
Est-ce qu’on peut avoir 2 envois simultanement ?
Kripke structure
On definit un alphabet, un etat, une transition.
Example
On utilise des booleens qu’on appelle des propositions atomiques
- On etiquete notre modele pour savoir si on peut atteindre un chemin
How to express finite behavior ?
Combien de propositions atomiques ?
3 (rouge, orange, vert)
Comment on exprime les comportements a l’infini ?
On utilise une logique
Linear Temporal Logic
On s’interesse aux operateurs:
- $U$: “vrai jusqu’a qu’autre chose soit vrai”
- $X$: “a la prochaine etape c’est vrai”
Globally
Finally
Next
Until
Retour au feu rouge
Automata for model checking
Buchi: Transformer une logique d’evenement en automate
Express property automaton
Automata approach for model checking
On a reussi a creer un modele pour Aut. A et Kripke. On fait un produit synchronise
Produit synchronise On a l’automate de la propriete
On a l’automate du systeme. Quand on lit $d_1$ et $r_1$, on doit s’assurer de lire la meme chose dans notre systeme, on supprime les chemins qui font diverger ces valeurs, par le produit cartesien.
On regarde cette automate, si on trouve une pastille noir qui s’appelle en boucle, on a un contre-exemple a notre propriete.
La reponse est oui
