Exemple : Contrôleur de feux

de circulation d’un carrefour

(cid:1) Problèmes: spécifier le fonctionnement d’un

contrôleur de feux tricolores d’un carrefour.

(cid:1) Les feux peuvent être :

(cid:3) Hors service (hs) : tous les feux sont au jaune

(cid:3) En service (es) : ils évoluent selon

rouge ↝↝↝↝ vert ↝↝↝↝ jaune ↝↝↝↝ rouge

(cid:3) Lorsque le feu est au rouge sur une voie, les

véhicules de cette voie ne peuvent s’engager

dans le carrefour

Leila Jemni Ben Ayed

GLII- Spécification et Vérification de Systèmes -

2014

Exemple : Contrôleur de feux

de circulation d’un carrefour

(cid:1) Propriétés souhaitées:

(cid:3) Condition de sécurité (safety) : les véhicules ne peuvent s

engager dans les deux voies simultanément.

(cid:3) Condition de vivacité (liveness) : les véhicules ne sont pas

bloqués infiniment sur l’une des (ou les deux) voies.

(cid:1) Ces propriétés sont décrites par :

((feuA=rouge)(cid:217) (feuB„ rouge))(cid:218) ((feuA„ rouge)(cid:217) (feuB=rouge))

(cid:1) Définition des couleurs des feux :

(cid:3) COULEUR = {rouge , jaune , vert}

(cid:3)

feuA ˛ COULEUR ,

feuB ˛ COULEUR

(cid:1) Définition de l’état des feux :

(cid:3)

ETAT = {es, hs}

etat ˛ ETAT

Leila Jemni Ben Ayed

GLII- Spécification et Vérification de Systèmes -

2014

Exemple : Contrôleur de feux

de circulation d’un carrefour

(cid:1) Caractérisation de l’état hors service

(cid:3) Etat = hs ⇔ feuA = jaune (cid:217)

feuB = jaune

(cid:1) Caractérisation de l’état en service

(cid:3) Etat = es ⇒ feuA = rouge (cid:218)

⇒

feuB = rouge

(cid:1) Caractérisation de la disponibilité (état en service)

rouge (cid:218)

(cid:1) L’ évolution des feux est décrite par une fonction

(cid:3) Etat = es ⇒ feuA „

feuB „

rouge

⇒

constante: Suiv ˛ Couleur ﬁ Couleur

(cid:1) Les opérations sur les feux de circulation sont:

(cid:3) Mise en service

(cid:3) Mise hors service

(cid:3) Changer feu

Leila Jemni Ben Ayed

GLII- Spécification et Vérification de Systèmes -

2014

Exemple : Contrôleur de feux

de circulation d’un carrefour

MACHINE

Carrefour

SETS

Couleur = {rouge, jaune, vert}

CONSTANT

Suiv

PROPERTIEES

˛ Couleur X Couleur (cid:217)

Suiv ˛

Suiv(rouge) = vert (cid:217)

Suiv(vert) = jaune (cid:217)

Suiv(jaune) = rouge

VARIABLES

feuA, feuB

DEFNITIONS

hs == feuA = jaune (cid:217)

service(aa, bb) = (aa = rouge (cid:217)

es == service(feuA, feuB)

feuB = jaune

(cid:217) bb „

rouge) (cid:218)

(aa „

rouge (cid:217)

(cid:217) bb = rouge)

INVARIANT

feuA, feuB ˛˛˛ ˛ Coulur X Couleur (cid:217)(cid:217)(cid:217) (cid:217) (hs (cid:218)(cid:218)(cid:218) (cid:218) es)

Leila Jemni Ben Ayed

GLII- Spécification et Vérification de Systèmes -

2014

(cid:217)

„

(cid:218)

„

(cid:217)

Exemple : Contrôleur de feux

de circulation d’un carrefour

INITIALISATION

feuA, feuB := jaune, jaune

OPERATIONS

Mise-en-service = PRE hs

THEN

END

Mise-hors-service = PRE es

ANY fa, fb WHERE

fa, fb ˛˛˛ ˛ Couleur X Couleur (cid:217)(cid:217)(cid:217) (cid:217) Service(fa, fb)

THEN

feuA := fa

feuB := fb

END

THEN

END

feuA, feuB := jaune, jaune

Leila Jemni Ben Ayed

GLII- Spécification et Vérification de Systèmes -

2014

Exemple : Controleur de feux

de circulation d’un carrefour

Changer-feu =

PRE es

THEN

ANY fa, fb WHERE

((fa = feuA (cid:217)

(fa = suiv(feuA) (cid:217)

service(fa, fb)

fb = suiv(feuB)) (cid:218)

fb = feuB) (cid:218)

fb = suiv(feuB))) (cid:217)

THEN

feuA, feuB := fa, fb

END

Leila Jemni Ben Ayed

GLII- Spécification et Vérification de Systèmes -

2014

(cid:217)

(cid:218)

(cid:217)

(cid:218)

(cid:217)