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
  $\ne$ 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