Cours 2: Systèmes De Transitions - Laboratoire IBISC

Cours 2: Systèmes de TransitionsFrancesco BelardinelliLaboratoire IBISC23 octobre 2014

Cours 2 - Vue d’Ensemble Systèmes de Transitions : classe de modèles pour la répresentation delogiciels et de l’hardware.IIExécutionsModélisation des systèmes (dépendants des données) Cours 3 : Parallélisme et CommunicationI EntrelacementI Variables Partagées

Resumé du Model Checking

Systèmes de Transitions Modèle pour décrire les comportements d’un système. Graphes orientés (digraphe) où les noeuds représentent les états et lesflèches modèlent les transitions. Etat :IIILa couleur courante d’un feu de circulation.Logiciel : les valeurs courantes des variables du programme le compteurdu programme.Hardware : la valeur courante de l’ensemble des registres avec les valeursdes entrées. Transition (changement d’état) :I Le passage d’une couleur à l’autre.I L’exécution d’une instruction du programme.I La modification des registres et des sorties par une nouvelle entrée.

Systèmes de TransitionsUn système de transitions TS est une tuple (S, Act, , I , AP, L) où S est un ensemble d’états Act est un ensemble d’actions S Act S est une rélation de transition I S est un ensemble d’états initiaux AP est un ensemble de propositions atomiques L : S 2AP est une fonction de marcage

Systèmes de TransitionsUn système de transitions TS est une tuple (S, Act, , I , AP, L) où S est un ensemble d’états Act est un ensemble d’actions S Act S est une rélation de transition I S est un ensemble d’états initiaux AP est un ensemble de propositions atomiques L : S 2AP est une fonction de marcageExamples de proposition atomique : x 0 y 200

Systèmes de TransitionsUn système de transitions TS est une tuple (S, Act, , I , AP, L) où S est un ensemble d’états Act est un ensemble d’actions S Act S est une rélation de transition I S est un ensemble d’états initiaux AP est un ensemble de propositions atomiques L : S 2AP est une fonction de marcageExamples de proposition atomique : x 0 y 200Notez que S et Act peuvent être finis ou infinis dénombrable. Un système de transitions TS est fini ssi S, Act et AP sont finis.α Notation : on écrit s s 0 à la place de (s, α, s 0 ) . Pour cheque formule propositionnelle φ, s φ ssi L(s) φ.

Le Rôle du Non-déterminismeDe façon générale, les systèmes de transitions sont non-déterministes. On a plusieurs états initiaux.α Pour chaque état s, on peut avoir plusieurs actions α telles que s s00pour quelque s . Pour chaque état s et action α, on peut avoir plusieurs états s 0 tels queαs s 0.

Un Distributeur Automatique des Boissonspayget sodaget beerinsert coinsodaτselectτbeerExercice 1Quels sont les ètats ? les états initiaux ? les actions ? les transitions ?

Propositions Atomiques ?Plusieurs choix de AP sont possible en dépendant des propriétés qu’on veutexprimer.Par défault, AP S L(s) {s}

Propositions Atomiques ?Plusieurs choix de AP sont possible en dépendant des propriétés qu’on veutexprimer.Par défault, AP S L(s) {s}.mais, si “le distributeur de boissons donne une boisson seulement si on paie.”

Propositions Atomiques ?Plusieurs choix de AP sont possible en dépendant des propriétés qu’on veutexprimer.Par défault, AP S L(s) {s}.mais, si “le distributeur de boissons donne une boisson seulement si on paie.” AP {paid, drink} L(pay ) L(soda) L(beer ) {paid, drink} L(select) {paid}

Successeur et Prédécesseur : définitionsPour un système de transitions TS, un état s et une action α,Post(s, α) Pre(s, α) Post(s) α{s 0 S s s 0}0 α0{s S s s}[Post(s, α)α ActPre(s) [Pre(s, α)α ActPost(C , α) [Post(s, α)s CPre(C , α) [Pre(s, α)s CPost(C ) [Post(s)s CPre(C ) [s CUn état s est terminal ssi Post(s) .Pre(s)

Déterminisme des Actions et des Propositions Une système de transition TS (S, Act, , I , AP, L) estaction-déterministe ssi pour tous s S, α Act, I 1et Post(s, α) 1 Une système de transition TS (S, Act, , I , AP, L) est AP-déterministessi pour tous s S, A 2AP , I 1et Post(s) {s 0 S L(s 0 ) A} 1 {z}successeurs de s avec le même marcage1. Le distributeur de boissons, est-il action-déterministe ? AP-déterministe ?2. action-déterminisme AP-déterminisme ?3. AP-déterminisme action-déterminisme ?

Le Rôle du Non-déterminismeLe non-déterminisme est une caracteristique importante ! pour modéliser la concurrence par entrelacementI Aucune hypothèse sur la vitesse relative des processus pour modéliser la liberté d’implémentationI On décrit seulement ce qu’un système doit faire, pas comment pour modéliser des systèmes sous-spécifiés, ou des abstractions desystèmes réelsIOn utilise des informations incomplètes (distributeur de boissons)

Modélisation des Circuitsx 0, r 0x 1, r 0x 0, r 1x 1, r 1yxr Représentation du système de transitions d’un circuit. x est la variable d’entrée, y la variable de sortie, et r le registre. λy (x r ) est la fonction de sortie. δr x r est la fonction d’évaluation du registre. Les action ne sont pas importantes (les transitions sont déterminées par lafonction δr ). La fonction de marcage L est déterminée par la fonction de sortie λy .

Propositions AtomiquesConsidèrez deux possibles marcages des états : Soit AP {x, y , r },L(x 0, r 1) {r }L(x 1, r 1) {x, r , y }L(x 0, r 0) {y }L(x 1, r 0) {x} Exemple de propriété : “une fois que le registre est un, il reste un” Soit AP {x, y }. Les valutations des registres sont désormais “invisibles”.L(x 0, r 1) L(x 1, r 1) {x, y }L(x 0, r 0) {y }L(x 1, r 0) {x} Exemple de propriété : “la sortie y est changée infiniment souvent”

Systèmes Dépendants de DonnéesLes actions des systèmes dépendants de données sont typiquement le résultatd’instructions conditionelles.if x%2 1 then x : x 1 else x : 2 xComment modéliser ça dans les TS ?

Le Distributeur Automatique de Boissons RevisitéLe distributeur compte le nombre des bouteilles et rend l’argents s’il est vide.Transitions abstraites :starttrue:coin true:refillstart select n soda 0:sgetn beer 0:bgetselect select Actioncoinret coinsgetbgetrefillEffet sur les variablesn soda 0 n beer 0:ret cointselectstartstartstartstartn soda : n soda 1n beer : n beer 1n beer : max; n soda : max

Répresentation à Graphe de Programmetrue : refilln soda 0 : sgetstarttrue : coinn soda 0 n beer 0 : ret coinn beer 0 : bgetselect

Notions Préliminaires Variable typée x Var avec une affectation η qui donne une valeursη(x) dom(x) à xIIpar exemple, dom(x) dom(y ) Zη(x) 17 et η(y ) 2 Eval(Var ) est l’ensemble des affectations η aux variables dans Var Cond(Var ) est l’ensemble des conditions booléennes sur VarII formules de la logique propositionnelle dont propositions ont la forme x D( 3 x 5) (y vert) (x 2 · x 0 ) L’effet des actions est donné par une fonction :EffectII:Act Eval(Var ) Eval(Var )par exemple, action α x : y 5 et affectation η(x) 17 et η(y ) 2Effect(α, η)(x) η(y ) 5 3 et Effet(α, η)(y ) η(y ) 2

Graphe de ProgrammeReprésentation de programmes avec conditions.Un graphe de programme PG sur un ensemble Var de variables typées est unetuple (Loc, Act, Effect, , Loc0 , g0 ) tel que, Loc est un ensemble de positions avec les positions initiales Loc0 Loc ; Act est un ensemble d’actions Effect : Act Eval(Var ) Eval(Var ) est la fonction d’effet Loc (Cond(Var ) Act) Loc est la rélation de transitionconditionelle g0 Cond(Var ) est la condition initialeg :αNotation : 0 dénote ( , g , α, 0 ) .

Distributeur de boissonsn soda 0 : sgettrue : refillstarttrue : coinn soda 0 n beer 0 : ret coinselectn beer 0 : bget Loc {start, select} avec Loc0 {start} Act {bget, sget, coin, ret coin, refill} Var {n soda, n beer } avec domaine {0, 1, . . . , max} Effect : Act Eval(Var ) Eval(Var ) est la fonction d’effetEffect(coin, η) ηEffect(ret coin, η) ηEffect(sget, η) η[n soda : n soda 1]Effect(bget, η) η[n beer : n beer 1]Effect(refill, η) [n beer : max, n soda : max] g0 (n beer max n soda max)

Des Graphes de Programme aux Systèmes de Transitions Stratégie de base : dépliageI état position courante affectation aux données ηI état initial position initiale satisfaisante la condition initial g0 Proposition et marcageI propositions : “à ” et “x D” pour D dom(x)I h , ηi est marqué par “à ” et toutes conditions qui sont vraies pour ηg :αα si 0 et g est vraie pour η, alors h , ηi h 0 , Effect(α, η)i

Système de Transition d’un Graphe de ProgrammeSoit PG (Loc, Act, Effect, , Loc0 , g0 ) un graphe de programme.Le système de transitions correspondant est défini commeTS(PG ) (S, Act, , I , AP, L)où S Loc Eval(Var )g :α 0 η gα S Act S est défini par la règle h , ηi h 0 , Effect(α, η)i I {h , ηi Loc0 et η g0 } AP Loc Cond(Var ) L(h , ηi) { } {g Cond(Var ) η g }

Sémantique Opérationnelle Structuréepremisse La notation conclusion signifie que. Si la proposition au dessus de la ligne (c.à.d., la prémisse) est vraie, alorsla proposition au dessous de la ligne (c.à.d., la conclusion) est vraie. Une proposition “si . . . , alors . . . ” pareille est appelée règles d’inférence. Si la prémisse est une tautologie, elle peut être omise (ainsi que le ligne). Dans ce dernier cas, la règle est aussi appelée axiome.

Systèmes de Transitions 6 Automates FinisContrairement aux automates finis, dans un système de transition : il n’existe pas d’état acceptant les ensemble d’états et d’actions peuvent être infinis dénombrables on peut avoir des ramifications infinies les actions peuvent être susceptibles de synchronisation (cf. prochaincours) le non-déterminisme a un rôle différentLes systèmes de transitions sont appropriées pour dècrire le comportement dessystèmes réactifs.

Système de Transition d’un Graphe de ProgrammeExercice 2Construisez le système de transitions correspondant au distributeur de boissonsabstrait.

Conclusions Systèmes de Transitions Le Rôle du Non-déterminisme Exécutions Modélisations des Circuits Systèmes Dépendants des Données Graphes de Programmes

Syst emes de Transitions Mod ele pour d ecrire les comportements d’un syst eme. Graphes orient es (digraphe) ou les noeuds repr esentent les etats et les eches mod elent les transitions. Etat: I La couleur courante d’un feu de circulation. I Logiciel : les valeurs courantes des variables du programme le compteur du programme.