# 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

:::danger
Il faut check toutes les relations et entralecements possibles (effets de bord, etc).
:::

:::success
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();
}

:::success
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


:::info
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


:::info
**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

:::info
**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