HackMD
ALGOREP: What is Model-Checking ? How to build a Model Checker ?
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
- 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
Pour passer de l'etat
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:
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
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
