Télécharger le fichier pdf d’un mémoire de fin d’études
Logique Temporelle a temps Linéaire
Nous rentrons avec cette section dans l’apres-modelisation. Que fait-on une fois le modele concu ? Nous sommes capables de donner le comportement d’un modele sous la forme d’une relation de transitions, mais comment en extrait-on des informations ?
Les informations que l’on souhaite extraire sont les proprietes du modele (ou du comportement du mod`ele). Une propri´et´ est donn´ee par la sp´ecification d’une formule logique, exprimant (lorsque la formule est valide) un comportement inclus dans celui du mod`ele sur lequel on veut avoir des infor-mations. Les propri´et´es que nous utilisons dans cette th`ese sont qualitatives c’est-`a-dire caract´eris´ees par le fait que l’on ne puisse r´epondre que par oui ou par non `a la question : “la propri´et´ est-elle valid´ee par le mod`ele ?”. La formule (mˆeme si elle utilise des informations quantitatives) d´enote une qualit´e pr´esente (ou non) dans le mod`ele.
Les concepts et notations des logiques modales utilis´ees en informatique sont issus de travaux en philosophie traitant des modalit´es comme la possibilit´e et l’obligation [HC68].
Nous allons pr´esenter en d´etail une de ces logiques, la logique temporelle `a temps lin´eaire (LTL), qui se r´ev`ele tr`es utile pour la sp´ecification de propri´et´es, permettant de raisonner sur l’ensemble des s´equences d’ex´ecution du mod`ele. Il est par exemple possible d’exprimer qu’un ´ev`enement inter-vient avant un autre, ou que dans le futur (sans plus de pr´ecisions) un ´ev`enement surviendra. Le s´equencement des actions est logique, c’est-`a-dire qu’aucune quantification (de dur´ee ou de distance, par exemple) n’est sp´ecifiable, contrairement `a d’autres logiques permettant de quantifier temporelle-ment l’enchaˆınement des actions, comme la logique MTL [Koy90]. Elle permet ´egalement de d´ecrire qu’un mod`ele fait effectivement quelque chose (propri´et´ de vivacit´e, ou liveness) et des propri´et´es plus simples `a v´erifier comme la d´etection d’erreurs, qui est ce que l’on appelle une propri´et´ de sˆuret´ (safety) : le syst`eme, quoi qu’il fasse, n’atteint pas un ´etat erron´e.
D´efinition 3 Syntaxe de LTL
Soit P A un ensemble de propositions atomiques et p ∈ P A. Les formules LTL sont obtenues par
la grammaire suivante : Φ ::= p | ¬Φ | Φ1 ∨ Φ2 | Φ1UΦ2 | N Φ (2.1)
Une formule LTL est vrai pour un mod`ele si et seulement si elle est vraie pour l’ensemble des ex´ecutions de ce mod`ele : comme nous allons le voir dans sa s´emantique, une formule est valid´ee de mani`ere r´ecursive a` partir de l’´etat initial, en parcourant un a` un tous les chemins d’ex´ecutions.
D´efinition 4 S´emantique de LTL
Soit P A un ensemble de propositions atomiques et p une de ces propositions ; σ = s0s1… une s´equence infinie d’´etats ; ν : S −→ 2P A une fonction d’´etiquetage, ν(si) d´efinissant donc l’ensemble des propositions atomiques v´erifi´ees par l’´etat si. σi |= Φ signifie que la formule Φ est satisfaite par σ `a la position i.
σ i |= p ssi p ∈ ν(si)
σ i |= ¬Φ ssi σi = Φ
σ i |= Φ1 ∨ Φ2 ssi σi |= Φ1 ou σi |= Φ2
σ i |= Φ1UΦ2 ssi ∃j > i tel que σj |= Φ2 et (∀k)(i 6 k < j ⇒ σk |= Φ1)
σ i |= N Φ ssi σi+1 |= Φ
Les autres op´erateurs usuels sont d´efinis en fonction de ces quatre fondamentaux : ∧ (et) a ∧ b = ¬(¬a ∨ ¬b)
⇒ (implique) a ⇒ b = ¬a ∨ b 3 (finalement) 3a = trueUa 2 (toujours) 2a = ¬3(¬a)
La d´efinition ci-dessus n’accepte que des s´equences infinies. Pour pouvoir appliquer cette d´efinition sur les s´equences finies, il suffit de r´ep´eter infiniment les ´etats ne poss´edant aucun successeurs, en les reliant par des transitions silencieuses (i.e. etiquet´es par ǫ, la lettre neutre pour la concat´enation).
Model checking DE LTL A L’AIDE DES AUTOMATES DE BUCHI
La s´emantique de LTL suppose que les ´etats sont etiquet´es. Dans le cas des syst`emes de transition temporis´es ce sont les transitions qui sont etiquet´ees. Pour se ramener `a une structure utilisable pour LTL, il convient donc soit de d´eporter l’information sur les ´etats, soit d’utiliser State/Event LTL [CCO+04], une variante supportant `a la fois les propositions atomiques sur les ´etats et les transitions.
Il est ´egalement possible de rep´erer un ´etat puits (i.e. un ´etat ne poss´edant pas de successeurs) en ´etiquetant cet ´etat par une ´etiquette sp´eciale puits. La d´etection d’un ´etat puits dans le comporte-ment d’un mod`ele se caract´erise par l’invalidation de la formule 2¬puits qui signifie «pour toutes les s´equences, il est toujours vrai que l’´etat n’est pas ´etiquet´ par puits» : lorsque cette formule est fausse, cela indique qu’il existe des s´equences pour lesquelles un ´etat est marqu´e par puits. Utiliser 3puits n’est pas correct pour la d´etection d’´etats puits, car cette formule signifie que toutes les ex´ecutions se terminent par cet ´etat. Il est par contre possible d’utiliser la formule ¬3puits «pour toutes les s´equences, il n’est pas possible d’arriver dans un ´etat marqu´e puits» qui est ´equivalente `a 2¬puits.
En reprenant le TTS donn´e en figure 2.2, on peut observer que la formule 2¬puits est fausse, car il existe un ´etat puits : q5 ; c’est ´egalement le cas pour la formule 3puits, car ce TTS poss`ede des s´equences infinies.
Pour conclure cette rapide introduction de la logique LTL, la formule suivante est typique des formes utilis´ees pour la v´erification des syst`emes r´eactifs : 2(c ⇒ 3a) (2.2)
Elle permet de savoir si a` tout ´ev`enement c, on peut trouver (pour toutes les s´equences possibles) un ´ev`enement a intervenant dans son futur, auquel cas, a peut ˆetre consid´er´ comme la r´eponse a` une requˆete c. Dans le syst`eme de la figure 2.2, cette formule est fausse car il existe une s´equence infinie qui l’invalide : q0.q3.q4.q8.(q6.q7)ω .
Nous savons donner (quoi que de mani`ere tr`es peu pratique pour l’instant) le comportement d’un mod`ele `a l’aide des TTS ; nous pouvons ´egalement sp´ecifier des propri´et´es de ce mod`ele par des formules de la logique LTL. Le lien entre les deux s’´etablit en transformant les formules LTL en automates de B¨uchi composables avec le mod`ele du comportement. Un automate de B¨uchi est diff´erent d’un automate classique car il permet de d´efinir un langage de mots infinis (contre un langage de mots finis pour les automates classiques). Un mot infini est aussi appel´ee trace, mais nous pr´ef´ererons le terme ex´ecution dans la suite.
En exprimant un mod`ele, nous donnons l’ensemble des ex´ecutions du syst`eme que l’on souhaite analyser. En exprimant une propri´et´e, nous donnons un ensemble d’ex´ecutions que l’on souhaite re-trouver dans le comportement du syst`eme. Un comportement, lorsqu’il est analys´e par une logique de chemins comme LTL, est formalisable par un ensemble de s´equences de transitions (ou traces, ou ex´ecutions). A chaque transition est associ´ee une lettre d’un alphabet Σ ; une s´equence de transitions d´efinit ainsi un mot, et l’ensemble des s´equences donnant le comportement du mod`ele d´efinit un lan-gage LΣ. Si le mod`ele est rep´er´ par M , alors LΣ(M ) donne son comportement, o`u Σ est l’ensemble des actions du mod`ele. De la mˆeme fa¸con, une propri´et´ P admet un langage LΣ(P ). Ainsi, v´erifier qu’une propri´et´ est valide pour un mod`ele revient `a v´erifier l’inclusion du comportement du mod`ele dans celui de la propri´et´ : LΣ(M ) ⊆ LΣ(P ) (2.3)
Deux m´ethodes sont alors possibles pour v´erifier cette inclusion.
– Soit directement par LΣ(P ) ∩ LΣ(M ) : si cette intersection est ´egale `a LΣ(M ), alors la propri´et´ est valide, elle ne l’est plus d`es qu’une ex´ecution du mod`ele n’est pas enti`erement englob´ee par le comportement de la propri´et´.
– Soit en niant la propri´et´ : LΣ(P ) ∩ LΣ(M ). Si l’intersection est vide alors la formule sp´ecifiant la propri´et´ P est vraie puisqu’il n’y a aucune ex´ecution satisfaisant la propri´et´ LΣ(P ).
La premi`ere m´ethode est plus compliqu´ee `a mettre en place puisqu’il faut pouvoir tester l’´egalit´ entre l’intersection et le mod`ele lui-mˆeme. Etape qui n’est pas n´ecessaire dans le deuxi`eme cas, puisqu’il est suffisant de tester la vacuit´e du langage.
La premi`ere m´ethode est plus compliqu´ee `a mettre en place puisqu’il faut pouvoir tester l’´egalit´ entre l’intersection et le mod`ele lui-mˆeme. Etape qui n’est pas n´ecessaire dans le deuxi`eme cas, puisqu’il est suffisant de tester la vacuit´e du langage.
Mis `a part les probl`emes de faisabilit´e et de complexit´ de l’intersection, de la compl´ementation, du test de langage vide et de l’´egalit´ de comportement, qui sont les op´erations potentiellement utilis´ees par les deux m´ethodes, la deuxi`eme m´ethode permet de connaˆıtre directement les traces qui falsifient la propri´et´e, desquelles il est possible d’extraire un contre-exemple, ce qui n’est pas possible avec la premi`ere m´ethode : seules les traces respectant la formule ´etant gard´ees.
Notre propos n’´etant pas de donner les d´etails permettant d’accomplir ces diff´erentes op´erations, nous en resterons a` ce niveau de d´etail. Pour plus de pr´ecision, nous recommandons la lecture de [CGP00] et de [DL07].
Le processus de v´erification est donn´e par la figure 2.3
Decidabilit´ de l’accessibilit´ des ´etats
L’ind´ecidabilit´ : une limite th´eorique de la v´erification automatique
Un des probl`emes les plus handicapant du model checking est la limite th´eorique de l’ind´ecidabilit´ de l’accessibilit´ d’un ´etat pour les formalismes capables de simuler une machine de Turing. Le r´esultat fondamental de Turing est que le test de l’arrˆet d’une machine de Turing est ind´ecidable : il n’existe pas de programme ex´ecutable sur une machine de Turing capable d’impl´ementer ce test. L’accessibilit´ d’un ´etat est une g´en´eralisation du test de l’arrˆet d’une machine de Turing : tester si un programme se termine (la machine s’arrˆete) revient a` tester si l’´etat dans lequel la machine s’arrˆete est accessible.
Pour savoir si un ´etat d’un syst`eme est accessible, il suffit de construire le comportement du syst`eme : si un ´etat est pr´esent dans la repr´esentation du comportement, cela signifie qu’il est accessible. Le caract`ere fini d’un comportement implique donc la d´ecidabilit´e de l’accessibilit´ de ses ´etats. De plus, lorsque l’accessibilit´ des ´etats d’un comportement est d´ecidable alors il existe un algorithme construisant une structure finie repr´esentant le comportement, qui lui peut ˆetre fini. Il faut bien faire attention : un comportement infini n’implique pas l’ind´ecidabilit´ de l’accessibilit´ de ses ´etats.
Puisqu’une repr´esentation finie du comportement est n´ecessaire pour appliquer la technique de v´erification par force brute (brute force) qu’est le model checking, l’ind´ecidabilit´ est donc une limite dont il nous faut pr´eciser les contours, et ce afin de connaˆıtre les syst`emes temps r´eel qu’il est possible de v´erifier sans tomber dans cette probl´ematique.
Comme nous allons le voir plus en d´etail au chapitre 4, la correction d’un syst`eme temps r´eel d´epend du respect de ses ech´eances. La dynamique de ces syst`emes implique quasiment syst´ematiquement l’utilisation d’un ordonnanceur capable de d´eterminer les tˆaches les plus prioritaires a` ex´ecuter. Il est possible que cet ordonnanceur soit autoris´e a` suspendre une tˆache en cours d’ex´ecution pour en laisser une autre, plus prioritaire, s’ex´ecuter. La tˆache suspendue ne l’est que temporairement et son ech´eance n’en est pas pour autant retard´ee. Ainsi la sp´ecification de tels syst`emes doit tenir le compte des horloges suspendues et de celles qui ne le sont pas. Les horloges sont des variables r´eelles sur lesquelles on peut appliquer soit une fonction d’incr´ementation synchrone au temps du syst`eme, soit les laisser telles quelles. Ceci nous fait rentrer dans le domaine des syst`emes hybrides, dont les r´esultats en termes de d´ecidabilit´ ne sont pas en la faveur d’une technique automatique.
Un syst`eme hybride est caract´eris´ par une dynamique a` la fois discr`ete et continue. L’un des formalismes les plus connus sont les automates hybrides form´es a` partir d’un automate classique sur lequel sont ajout´ees des informations et des contraintes de progr`es de variables continues. En limitant l’expression des fonctions d’´evolution des variables continues, on obtient diff´erentes classes d’automates hybrides. Voici un court aper¸cu des r´esultats de d´ecidabilit´ li´es aux automates hybrides en fonctions des limitations impos´ees aux fonctions d’´evolutions.
Automates temporis´es [ACD90]. Cette classe est l’une des plus restreintes des automates hy-brides. La fonction d’´evolution des horloges est limit´ee a` une d´eriv´ee constante ´egale pour toutes les horloges, qui sont les seules variables continues du formalisme. L’accessibilit´ est d´ecidable [AD94].
Les automates hybrides initialis´es. Les classes d’automates qui vont suivre poss`edent la ca-ract´eristique d’ˆetre initialis´ees : lorsque l’´evolution des variables continues change (par une transition discr`ete), les variables sont r´einitialis´ees (`a une valeur arbitraire).
Automates initialis´es a` multi-vitesses [ACHH93],[NOSY93] [HKPV95]. Cette classe autorise des ´evolutions diff´erentes pour les variables continues, mais toutes ces ´evolutions sont des d´eriv´ees premi`ere (vitesse) fixe (une valeur de vitesse possible). L’accessibilit´ pour cette classe est d´ecidable. Les automates de cette classes sont tous traduisibles en automates temporis´es temporellement bisimi-laires (la notion de bisimulation est d´efinie dans la section suivante).
Automates initialis´es rectangulaires [HKPV95]. Cette classe est une g´en´eralisation de la pr´ec´edente car elle autorise un intervalle de vitesse au lieu d’une seule valeur d´efinissant la vitesse d’´evolution des variables continues.
Puisque les automates sont initialis´es, il n’est pas possible de sp´ecifier que l’´evolution d’une variable (horloge) s’interrompt et reprend normalement apr`es un d´elai arbitraire. Pour cela il faut autoriser la condition d’initialisation.
Un r´esultat de [HKPV95], montre qu’en enlevant la condition d’initialisation, mais en restreignant avec : l’invariant est constant, non strict et born´e ; lors du tir d’une transition discr`ete les variables peuvent soit ˆetre remises `a z´ero, soit conserver leur valeur ; la garde est non stricte et born´ee ; au plus une seule variable n’est pas une horloge (la vitesse d’une horloge est constante et ´egale `a 1) ; l’accessibilit´ pour cette restriction drastique des automates hybrides non n´ecessairement initialisable est ind´ecidable si la variable qui n’est pas une horloge admet deux vitesses : 1 (similaire `a une horloge) et x ∈ Q \ {1}.
Les horloges marquant la pr´eemption des tˆaches doivent poss´eder deux vitesses : 0 et 1, ce qui rentre dans ce r´esultat l’ind´ecidabilit´ de l’accessibilit´e des ´etats.
Ceci est vrai sur tous les formalismes poss´edant une caract´eristique ´equivalente et notamment pour les automates temporis´es `a chronom`etres [CL00], les r´eseaux de Petri ordonnanceurs [RD02], les r´eseaux de Petri pr´eemptifs [BFSV03], les r´eseaux de Petri temporel `a hyper-arcs inhibiteurs [RL04] et les r´eseaux de Petri temporels `a chronom`etres [BLRV05].
Ce probl`eme l’ind´ecidabilit´ n’est pas r´eserv´ a` l’expression des variables continues, car pour le formalisme des r´eseaux de Petri temporels, que nous allons pr´esenter dans la suite, l’accessibilit´ des ´etats est ind´ecidable lorsque le r´eseau de Petri sous-jacent (sans informations temporelles) est non-born´e. Nous verrons cela plus en d´etail dans la suite de ce chapitre.
Bisimulation
Pouvoir raisonner sur des syst`emes mod´elis´es `a des niveaux d’abstractions ou de raffinements diff´erents exige souvent de savoir les comparer. L’´equivalence langage ou l’isomorphisme sont utilisables pour comparer deux relations de transition. Il est par exemple possible d’employer l’´equivalence langage lors d’un processus de mod´elisation par raffinements successifs, le raffinement n’´etant acceptable que s’il est ´equivalent `a son abstraction. L’isomorphisme n’est pas adapt´e pour ce genre de m´ethodologie, car alors la marge de manœuvre laiss´ee `a une abstraction ou `a un raffinement est restreinte `a la seule possibilit´e de renommer les termes utilis´es dans le mod`ele. L’´equivalence langage est par contre trop faible pour v´erifier que les choix (les branchements) au cours d’une ex´ecution sont possibles aux mˆeme endroits dans les deux relations de transitions compar´ees. Elle ne pr´eserve pas non plus la notion de blocages. Dans ce cas, l’isomorphisme est ´egalement une ´equivalence peu int´eressante, car mˆeme si les branchements sont bien pr´eserv´es, aucune libert´ n’est permise : les deux comportements doivent ˆetre identiques au nom pr`es.
La notion de bisimulation est une notion d’´equivalence interm´ediaire [San04] tr`es utile pour la com-paraison de comportements et r´epondant `a la probl´ematique par raffinements successifs. De mani`ere g´en´erale, elle permet de v´erifier que deux comportements sont «similaires» : si un syst`eme fait une action, alors l’autre syst`eme fait ´egalement cette action et r´eciproquement. De plus, il est ´egalement possible de se servir d’une variante «faible» de cette abstraction, ne prenant en compte que les actions non silencieuses (observables), pour d´eterminer si une propri´et´e, cod´ee sous la forme d’un automate, est valide pour un comportement (dont on aura rendue non observables les actions n’apparaissant pas dans la propri´et´e) : si celui-ci est faiblement bisimilaire `a la propri´et´e, cela signifie que la propri´et´ est valide pour ce comportement.
Un langage formel pouvant ˆetre d´efini par l’ensemble de comportements qu’il peut exprimer, cette ´equivalence peut ´egalement servir pour comparer deux formalismes.
Il est possible d’´etendre cette ´equivalence pour l’adapter `a la comparaison de TTS . On obtient ainsi la bisimulation temporis´ee [Yi90], notion plus fine que la bisimulation, particuli`erement adapt´ee pour comparer deux formalismes utilisant une notion de temps.
R´eseaux de Petri temporels `a permissions et inhibitions
Les r´eseaux de Petri temporels `a permissions et inhibitions (ipTPN ) ´etendent les TPN `a l’aide de deux nouvelles relations entre les transitions. Afin de comparer ce nouveau formalisme avec ses pr´ed´ecesseurs, nous utilisons un alphabet d’actions et une fonction d’´etiquetage des transitions. I+ est l’ensemble des intervalles `a bornes rationnelles non-n´egatives. Si i ∈ I+, ↓i donne sa borne inf´erieure, et ↑ i sa borne sup´erieure si i est born´ee, ou ∞ dans le cas contraire. Pour tout θ ∈ R+, i −. θ est l’intervalle {x − θ | x ∈ i ∧ x > θ}.
D´efinition 15 Un r´eseau de Petri temporel a` permissions et inhibitions ( ipTPN en abr´eg´e) est un
n-uplet P , T , Pre, Post, m0, Is, F , A, Σǫ, L dans lequel :
– P , T , Pre, Post, m0, Is, Σǫ, L est un r´eseau de Petri temporel,
– F ⊆ T × T est la relation d’inhibition (F pour forbid en anglais),
– A ⊆ T × T est la relation de permission (A pour allow en anglais),
– Σ est un ensemble fini d’actions (ou ´etiquettes), qui ne contient pas l’action silencieuse ǫ,
– L : T → Σǫ est une fonction appel´ee fonction d’´etiquetage.
(t1, t2) ∈ F est not´e t1−◦ t2 (t1 inhibe (ou interdit le tir de) t2) et (t1, t2) ∈ A est not´e t2−• t1 (t1 autorise (ou permet) le tir de t2). Une transition sera dite T-sensibilis´ee si z´ero appartient `a son intervalle de tir. Dire d’une transition qu’elle est tirable est ´equivalent `a dire qu’elle est T-sensibili ´ee dans le formalisme des TPN (mais pas dans celui des ipTPN !).
(t1, t2) ∈ F est not´e t1−◦ t2 (t1 inhibe (ou interdit le tir de) t2) et (t1, t2) ∈ A est not´e t2−• t1 (t1 autorise (ou permet) le tir de t2). Une transition sera dite T-sensibilis´ee si z´ero appartient `a son intervalle de tir. Dire d’une transition qu’elle est tirable est ´equivalent `a dire qu’elle est T-sensibili ´ee dans le formalisme des TPN (mais pas dans celui des ipTPN !).
D´efinition 16 La s´emantique de l’ ipTPN P , T , Pre, Post, m , I , F , A, Σǫ , L est le syst`eme de 0s transitions temporis´ S, (m0, Is0), Σ, → o`u :
– Is0 est la fonction Is restreinte aux transitions sensibilis´ees par m0
– les ´etats de S sont les paires (m, I) dans lesquelles m est un marquage et I : T → I+ associe un intervalle temporel `a chaque transition sensibilis´ee par m, L (t)
– (m, I) −−→ (m′, I′) ssi t ∈ T et
1) Pre(t) 6 m
2) 0 ∈ I(t)
3) (∀k ∈ T )(Pre(k) 6 m ∧ 0 ∈ I(k) ⇒ ¬(k−◦ t))
4) (∀k ∈ T )(Pre(k) 6 m ∧ 0 I(k) ⇒ ¬(k−• t))
5) m′ = m − Pre(t) + Post(t)
6) (∀k ∈ T \ {t})(Pre(k) 6 m − Pre(t) ⇒ I′(k) = I(k))
7) (∀k ∈ T )(Pre(k) 6 m′ ⇒ I′(k) = Is(k))
Les ipTPN pour rendre les TPN composables
Nous avons tous tendance, face `a un probl`eme complexe, `a vouloir le d´ecomposer en sous-parties plus simples. Non que la complexit´ du syst`eme s’en trouve r´eduite, mais il est ainsi plus facile d’appr´ehender les aspects de ce syst`eme sous des angles plus accessibles. C’est la base des m´ethodes de conception incr´ementales, bas´ees sur l’ajout successif des sous-syst`emes ainsi produits. La m´ethodologie que nous utilisons dans cette th`ese est particuli`erement sujette `a de telles d´ecompositions.
Le mod`ele des r´eseaux de Petri admet intrins`equement un fonctionnement parall`ele (ou concurrent) et peut ultimement ˆetre d´ecompos´ jusqu’`a n’avoir plus qu’une seule transition (et toutes les places n´ecessaires a` ses pr´e/post-conditions) par composant. Cette d´ecomposition n’est pas toujours la plus ad´equate en terme de conception, mais sa faisabilit´e ne pose aucun probl`eme th´eorique. L’une des meilleures d´emonstrations de ce fait est le langage alg´ebrique a` base de boˆıtes Petri, le Petri Box Calculus [BDH92], o`u l’´el´ement de base est une transition avec une place en entr´ee et en sortie, qui va ˆetre manipul´e par des op´erateurs de composition (proches de ceux que nous venons de d´efinir) tels que l’on puisse construire plus ou moins ais´ement tout type de r´eseaux.
S’il est reconnu que les r´eseaux de Petri sont ais´ement composables, il est par contre ´egalement connu que rajouter une information temporelle sur les transitions restreint fortement les possibilit´es de composition tr`es larges qui existaient dans le cadre atemporel. En effet, comment composer des transitions portant un intervalle temporel non trivial ? Comment concilier des intervalles diff´erents ? La m´ethode la plus courante, nous venons de le voir, est de prendre l’intersection des intervalles temporels des transitions compos´ees. Mais ceci n’est qu’un pis-aller posant plus de probl`emes qu’il n’en r´esout. Cela signifie que l’on ne peut pas toujours effectuer la composition : si les intervalles sont disjoints le r´esultat serait incoh´erent. Mais, plus grave, cette composition ne pr´esente pas, comme nous allons le voir, de «bonnes propri´et´es» en ce qui concerne la v´erification et la mod´elisation.
Plutˆot que d’´etudier la composition dans sa totalit´e, nous allons utiliser la restriction suivante : D´efinition 24 Composition parall`ele //
Soient deux r´eseaux de Petri etiquet´es Na = P a, T a, Prea, Posta, m0a, Isa, F a, Aa, Σaǫ, La et Nb = P b, T b, Preb, Postb, m0b, Isb, F b, Ab, Σbǫ, Lb .
Si (∀p ∈ P a)(∀p′ ∈ P b)(La(p) =ǫ Lb(p′)), alors la composition Na ⊙ Nb pourra etre notée par
Na//Nb . L’opérateur // est dit operateur de composition parallèle.
Le mod`ele des r´eseaux de Petri admet intrins`equement un fonctionnement parall`ele (ou concurrent) et peut ultimement ˆetre d´ecompos´ jusqu’`a n’avoir plus qu’une seule transition (et toutes les places n´ecessaires a` ses pr´e/post-conditions) par composant. Cette d´ecomposition n’est pas toujours la plus ad´equate en terme de conception, mais sa faisabilit´e ne pose aucun probl`eme th´eorique. L’une des meilleures d´emonstrations de ce fait est le langage alg´ebrique a` base de boˆıtes Petri, le Petri Box Calculus [BDH92], o`u l’´el´ement de base est une transition avec une place en entr´ee et en sortie, qui va ˆetre manipul´e par des op´erateurs de composition (proches de ceux que nous venons de d´efinir) tels que l’on puisse construire plus ou moins ais´ement tout type de r´eseaux.
S’il est reconnu que les r´eseaux de Petri sont ais´ement composables, il est par contre ´egalement connu que rajouter une information temporelle sur les transitions restreint fortement les possibilit´es de composition tr`es larges qui existaient dans le cadre atemporel. En effet, comment composer des transitions portant un intervalle temporel non trivial ? Comment concilier des intervalles diff´erents ? La m´ethode la plus courante, nous venons de le voir, est de prendre l’intersection des intervalles temporels des transitions compos´ees. Mais ceci n’est qu’un pis-aller posant plus de probl`emes qu’il n’en r´esout. Cela signifie que l’on ne peut pas toujours effectuer la composition : si les intervalles sont disjoints le r´esultat serait incoh´erent. Mais, plus grave, cette composition ne pr´esente pas, comme nous allons le voir, de «bonnes propri´et´es» en ce qui concerne la v´erification et la mod´elisation.
Plutˆot que d’´etudier la composition dans sa totalit´e, nous allons utiliser la restriction suivante : D´efinition 24 Composition parall`ele //
Soient deux r´eseaux de Petri etiquet´es Na = P a, T a, Prea, Posta, m0a, Isa, F a, Aa, Σaǫ, La et Nb = P b, T b, Preb, Postb, m0b, Isb, F b, Ab, Σbǫ, Lb .
Si (∀p ∈ P a)(∀p′ ∈ P b)(La(p) =ǫ Lb(p′)), alors la composition Na ⊙ Nb pourra etre notée par
Na//Nb . L’opérateur // est dit operateur de composition parallèle.
|
Table des matières
1 Introduction
1.1 Organisation de la th`ese
2 Eléments contextuels a la vérification par model checking
2.1 Etapes du model checking
2.2 Systèmes de transitions temporises
2.3 Logique Temporelle a temps Lineaire
2.4 Model checking de LTL a l’aide des automates de Buchi
2.5 Decidabilite de l’accessibilite des etats
2.6 Bisimulation
2.7 R´eseaux de Petri temporels
2.7.1 D´efinitions
2.7.2 S´emantique
2.7.3 D´ecidabilit´e
2.8 Des classes pour les TPN
2.8.1 Graphe de classe lin´eaire
2.9 Extensions
2.9.1 read arcs
2.9.2 arcs inhibiteurs
2.9.3 Arcs chronom`etres
2.10 Conclusion
3 Réseaux de Petri a permissions et inhibitions
3.1 Introduction – Motivation de l’extension
3.2 R´eseaux de Petri temporels `a permissions et inhibitions
3.3 Expressivit´e
3.3.1 Introduction
3.3.2 Composition des ipTPN
3.3.3 Les ipTPN pour rendre les TPN composables
3.3.4 Les ipTPN pour coder les TA
3.4 Abstractions de l’espace d’´etats pour les ipTPN
3.4.1 Graphe de classes (`a temps) lin´eaire
3.4.2 Graphe de classes lin´eaires fortes
3.5 Conclusions
4 Le langage Pola
4.1 Introduction
4.1.1 Objectif
4.1.2 Un langage sp´ecifique `a un domaine
4.1.3 Syst`emes temps r´eel
4.1.4 Caract´erisation du domaine
4.1.5 des langages d´edi´es existants
4.2 Description du langage
4.2.1 Groupes de tˆaches et points de r´eordonnancement `a la Osek
4.2.2 partitionnement `a la Arinc 653
4.3 Conclusion
5 S´emantique de Pola
5.1 Le m´eta-mod`ele Pola
5.2 Pr´eprocesseur de r´eseaux de Petri
5.3 Notation graphique
5.3.1 Associ´ee aux arcs
5.3.2 Associ´ee `a tout ´el´ement
5.4 S´emantique par traduction
5.4.1 Syntaxe textuelle des r´eseaux de Petri `a permission/inhibition
5.4.2 system et ressources
5.4.3 Traduction d’une tˆache
5.4.4 Traduction d’une action
5.4.5 Traduction d’une p´eriode
5.4.6 Traduction d’un offset
5.4.7 Traduction d’une ´ech´eance
5.5 Traduction d’une politique d’ordonnancement
5.5.1 Sur les politiques dynamiques
5.6 Traduction d’une allocation
5.6.1 Utiliser ou ne pas utiliser la politique d’ordonnancement, telle est la question
5.6.2 La traduction
5.7 Assemblage des ´el´ements
5.7.1 S´equencement et priorit´e des ´ev`enements
5.7.2 Gestion de l’ind´eterminisme des actions / p´eriodes / offsets
5.7.3 Composition des ´el´ements Pola
5.8 Conclusion
6 L’outil Pola : Etudes de cas et exp´erimentations
6.1 Architecture
6.1.1 Propri´et´es
6.2 Pr´esentation des mod`eles
6.2.1 Mod`eles utilisant des groupes Osek
6.2.2 Base
6.2.3 Variation 1
6.2.4 Variation 2
6.2.5 Variation 3
6.2.6 Variation 4, 4′ et 4′′
6.3 Influences des param`etres
6.4 Cas d’´etude : Arinc 653
6.4.1 Base
6.4.2 Variation 1
6.4.3 Variation 2
6.4.4 Les variations de la variation 3
6.4.5 R´esultats
6.5 Corrections d’erreurs et raffinages quantitatifs
6.5.1 Une erreur dans le mod`ele Osek
6.5.2 Analyse quantitative manuelle par raffinages successifs
6.5.3 Comparaison avec l’outil Times
6.6 Conclusion
7 Conclusion
7.1 Contributions
7.2 Perspectives
Télécharger le rapport complet
