Modèles Génériques en Réseaux de Petri Bien Formés pour le … · aux concepteurs des briques de modélisation et, d’autre part, de pouvoir exploiter les différentes techniques

Modèles Génériques en Réseaux de Petri Bien Formés pour le Contrôle Discret des Trains

Autonomes Yuchen Xie, Manel Khlif-Bouassida, Armand Toguyéni

Centrale Lille, CRIStAL, UMR 9189 59650 Villeneuve-d’Ascq, France

Univ. Lille Nord de France, F-59650, Lille, France {yuchen.xie, manel.khlif-bouassida, armand.toguyeni}@centralelille.fr

Résumé L’automatisation et l’adoption d’ERTMS (European Rail Traffic Management

System) sont deux solutions pour augmenter la capacité des systèmes ferroviaires, et pour améliorer leur sécurité. Cette étude est une contribution à une méthodologie permettant le développement de contrôleurs logiques discrets, pour mettre en œuvre le concept de train autonome. Ce travail concerne plus particulièrement, l’étape de modélisation de ces contrôleurs, en se basant sur les Réseaux de Petri Bien Formés (Well-formed Petri Nets, WN). Lors de la modélisation, les exigences du système ferroviaire et la nécessité de vérifier formellement certaines propriétés cruciales (absence de risques de collision …) sont prises en compte. Nous proposons des modèles génériques afin, d’une part, d’offrir aux concepteurs des briques de modélisation et, d’autre part, de pouvoir exploiter les différentes techniques de vérification offertes par ce formalisme. En effet, la complexité des systèmes ferroviaires nécessite de développer des techniques de vérification efficaces afin de réduire les problèmes d’explosion combinatoire qu’elle engendre.

1 Introduction Le train autonome consiste à faire circuler des trains sur un réseau ferroviaire sans mécanicien à

bord. Cela nécessite l’automatisation des fonctions de conduite du train et de surveillance de son fonctionnement. Le train autonome permettra d’augmenter la fréquence des circulations ainsi que la sécurité des systèmes ferroviaires, la diminution de la consommation énergétique et une dépendance moindre de la disponibilité d’une ressource comme les mécaniciens.

Cette étude fait partie d'une méthodologie permettant le développement systématique et rigoureux de contrôleurs discrets nécessaires à l'automatisation ferroviaire. La méthodologie que nous

MSR 2017, 11ème Colloque sur la Modélisation des Systèmes Réactifs 15-17 novembre 2017, Marseille, France

1

développons est, d’abord, basée sur la modélisation formelle des fonctions de contrôle discrets à bord et au sol (au niveau de l’infrastructure). Cette modélisation doit permettre de garantir la sécurité (safety) du système notamment par le biais d’une vérification formelle. Le travail présenté ici concerne plus particulièrement la phase de modélisation. Elle est basée sur l’exploitation du formalisme des Réseaux de Petri (RdP). Nous avons choisi d’utiliser les Réseaux de Petri Bien Formés (Well-formed Petri Nets, WN dans la suite de ce papier) comme formalisme de modélisation pour leur pouvoir d’abstraction et pour bénéficier des différentes possibilités de vérifications offertes par ce formalisme.

Cet article est structuré comme suit : Dans la deuxième partie, nous présentons les principaux composants d’un système ferroviaire, ses principales fonctions et nos hypothèses de travail. La troisième partie propose un état de l’art sur les approches de modélisation des systèmes ferroviaires basés sur les RdP et une justification de notre choix des WNs. Dans la quatrième partie, nous présentons le formalisme et les caractéristiques principales des WNs. Dans la cinquième partie, nous proposons des motifs (patterns) de modélisation permettant de construire les fonctions mises en œuvre dans le contrôle discret des systèmes ferroviaires. Dans la partie 6, nous illustrons l'utilisation de ces motifs sur un cas d’étude de système ferroviaire. Nous finissons par des conclusions et des perspectives.

2 Composants d’un système ferroviaire et contexte d’exploitation

Cette étude concerne le contrôle de plusieurs trains sur une ligne ferroviaire. Ce contrôle est basé sur la notion d’autorisation de mouvements ou MA (Movement Authorization), qui est un concept classique utilisé par les systèmes de contrôle ferroviaire. Les MAs sont données par les systèmes de contrôle de l’infrastructure au sol. Nous présentons d’abord, les principaux composants d’un système ferroviaire et ensuite, les principes des systèmes de contrôle et de signalisation ferroviaire. Dans la suite du papier, nous utilisons le terme « circulation ». Une circulation est l’affectation d’un itinéraire et d’un ordonnancement prévisionnel (dates de passage par des nœuds ferroviaires) à un train donné.

2.1 Lignes ferroviaires et cantons Les lignes ferroviaires relient différentes gares ferroviaires. Normalement toutes les circulations

d’une ligne ferroviaire se déplacent dans le même sens. Une ligne ferroviaire est divisée en plusieurs sections de voie appelées cantons comme indiquée dans la Figure 1.

Figure 1 : Ligne ferroviaire en cantons et principe du contrôle par ETCS-2

La notion de canton est essentielle pour garantir la sécurité des circulations ferroviaires. En effet, cette notion a été introduite pour empêcher les collisions entre les circulations. Le canton est une ressource critique qui ne peut être utilisée que par une seule circulation à la fois. Mais le grand nombre de cantons d’une ligne réelle est l’un des facteurs de complexité du point de vue de la modélisation et de la vérification discrète.

Fin d’autorisation de mouvement (EOA)

Canton NCanton N-1Canton N-2

Autorisation de movement (MA)

Train 1

Direction

Radio Block Centre (RBC)Position de Train, Requête de MA.,…

Train 2

Eurobalises

Vitesse

Gare 2Gare1Canton 1 Canton N-3


2

2.2 Contrôle des lignes ferroviaires basé sur le standard ETCS-2 L’Union Européenne vise à uniformiser les systèmes de signalisation et de contrôle dans les

différents états, afin de garantir l’interopérabilité des systèmes ferroviaires de chaque état et d’accroitre la sécurité. Pour cela, le système ERTMS (European Rail Traffic Management System) a été défini, dont l’une des composantes principales est l’ETCS (European Train Control System) (UNISIG, 2006). Les lois Européennes exigent la mise en œuvre de ce système sur toute nouvelle ligne et son déploiement progressif sur les anciennes lignes.

ETCS est défini selon quatre niveaux (niveaux 0 à 3). Actuellement, ERTMS/ETCS niveau 2 (ETCS-2) a été mis en service sur plusieurs lignes ferroviaires à grande vitesse en Europe. Il utilise les Eurobalises pour aider à la localisation des trains et, la transmission radio continue GSM-R (Global System for Mobile Communications – Railway) pour les échanges de données entre l’infrastructure au sol et les trains. Cette étude est basée sur l’ETCS-2 qui est le premier niveau exigeant une gestion explicite des MAs. Comme le montre la Figure 1, ETCS-2 offre les fonctions principales suivantes :

Côté infrastructure : Le Radio Block Center (RBC) est un centre de contrôle avec lequel les circulations discutent par ondes radios. Il répond aux requêtes des circulations en leur fournissant leurs MAs. Une MA est la liste des cantons d’une ligne sur lesquels une circulation est autorisée à se déplacer à une date donnée. Cette liste est complétée par des limitations de vitesses à respecter sur chaque canton. Normalement, la circulation est autorisée à se déplacer entre sa position courante et le canton antérieur à celui sur lequel est positionnée la circulation qui la précède sur la ligne. Ce canton constitue la fin d’autorisation de mouvement (EOA, End Of Authority en Anglais). Pour la première circulation de la ligne, l’EOA est le dernier canton de la ligne.

À bord : Chaque circulation envoie régulièrement sa position au RBC correspondant. Elle fait également régulièrement des demandes de MA. Pour une MA donnée, l’EVC (European Vital Computer), calculateur embarqué, calcule également un profil de vitesse pour que la circulation puisse respecter son EOA.

2.3 Principales hypothèses de fonctionnement définissant le cadre de l’étude

Cette étude considère un ensemble d'hypothèses simplificatrices pour la gestion de plusieurs circulations simultanées sur une ligne ferroviaire. Le but de ces simplifications est de réduire la complexité des modèles afin d’avoir la capacité de les présenter dans un nombre de pages limité. Les principales hypothèses sont :

1. Nous considérons qu’une ligne ferroviaire n’a qu’une gare d’entrée et une gare de sortie. Les circulations ne peuvent pas se dépasser sur la ligne (fonctionnement de type FIFO).

2. Nous considérons qu’un seul RBC gère la totalité d’une ligne ferroviaire. Cette hypothèse nous sert à ne pas considérer le problème de commutation entre RBC (la fonction « RBC Handover ») qui alourdirait considérablement la compréhension de nos modèles.

3. Les MAs sont réduites à la donnée du canton EOA. Ainsi les autres paramètres d’une MA ne sont pas pris en compte dans notre étude.

4. Chaque fois qu'une circulation sort d’un canton, elle reçoit sa position courante d'une Eurobalise. Immédiatement, elle envoie un rapport de positionnement au RBC. Dans le standard, les positions donnant lieu à l’envoi d’un rapport sont définies dans la MA donnée par le RBC.

5. Chaque rapport de positionnement reçu par un RBC est également considéré comme une requête de demande de MA. Le RBC met à jour la position de la circulation et génère immédiatement une nouvelle MA.


3

3 Modélisation d’un système ferroviaire basée sur les Réseaux de Pétri Colorés

Les Réseaux de Petri sont un formalisme utilisé depuis plus d’un demi-siècle et ont montré leur capacité à modéliser des systèmes concurrents et complexes. Les Réseaux de Petri Colorés de Jensen (CPN) sont l’extension des RdP la plus largement utilisée, car intégrant données structurées, hiérarchie, et temps (van der Aalst et al., 2013).

Dans la littérature, plusieurs études ont utilisé les CPN pour modéliser et analyser des contrôleurs discrets pour les systèmes ferroviaires (Janczura 1999 ; Ratzer et al., 2003 ; Jensen et al., 2007 ; van der Aalst et al. 2013). Ces études exploitent toutes la hiérarchie et la modularité de CPN pour définir différents niveaux de contrôle (Jansen et al. 1998 ; Meyer zu Hörste 1999 ; Žarnay 2004), voire pour définir différentes catégories de contrôleurs selon les composants du système (Žarnay 2004 ; Xie et al., 2016). Dans (Vanit-Anunchai 2009 ; Vanit-Anunchai 2010 ; Vanit-Anunchai 2014), l’auteur utilise les CPNs pour modéliser les enclenchements (conditions de réalisation d’itinéraires concurrents dans les nœuds d’aiguillages) d’un système ferroviaire. L'avantage de ce travail est de proposer des modèles CPN qui sont indépendants de la structure et de la taille du système ferroviaire.

Mais toutes ces études se sont focalisées que sur la modélisation, limitant la vérification à la seule utilisation de la simulation. Elles n’ont pas pris en compte l’exigence de plus en plus forte de vérification formelle afin de garantir la sécurité du système commandé. Ainsi, elles exploitent toutes des extensions de CPN basées sur ML son langage support. Par exemple dans (Xie et al., 2016) les auteurs utilisent des listes ML pour implémenter les files de trains sur une ligne. Ces structures de données facilitent la modélisation mais ne permettent pas de faire de vérification, car elles sont difficiles de se transformer en états du graphe d’accessibilité.

Figure 2 : Différentes méthodes d’analyse des RdPC

Comme le montre la partie gauche de la Figure 2, la manière la plus intuitive d'analyser un RdP est de générer le graphe d'accessibilité qui permet de vérifier les propriétés requises. Bien qu'elle soit possible en théorie, l'application de cette méthode est généralement limitée par des problèmes d'explosion combinatoire. Une manière de lutter contre cette explosion combinatoire serait de réduire d'abord le modèle RdPC initial avant de construire le graphe d'accessibilité du modèle réduit. Cette méthode exige que les règles de réduction utilisées garantissent la conservation, dans le modèle réduit, des propriétés que l’on cherche à vérifier dans le modèle initial. Cependant, il existe très peu de travaux proposant des règles de réduction applicables à n’importe quel type de RdPC et chacune d'elles a ses propres contraintes d’application. Par exemple, les règles de réduction proposées dans (Esparza & Hoffmann 2016) ne s'appliquent qu'aux RdPC de type workflots à choix libre (free-choice workflow nets), dans le but de maintenir la « soundness ». Dans le cas général, la seule solution possible consiste

Exigences duSystème Ferroviaire

ModèlesRéseauxdePetri Coloré(RdPC) ModèlesRéseauxdePetriBienFormés(WN)

Graphed'accessibilité

RdP P/TDépliésWNRéduits

RdP P/TRéduits

InvariantsColorés

GraphedesMarquagesSymboliques

Modélisation

TransformationdeModèle

Analyse etVérification

RdPC Réduits

InvariantsduRdP P/T

Réduction DépliageRéduction

Reduction


4

à déplier le RdPC, afin de le transformer en son RdP P/T équivalent et enfin à y appliquer les règles de réduction qui ont été développées pour les RdP P/T (Berthelot & Lri-Iie 1986 ; Murata, 1989). Le problème de cette méthode est que l’on retombe dans la problématique de l’explosion combinatoire à laquelle on est confronté dès l’étape de dépliement pour un système complexe, comme peuvent l’être les systèmes ferroviaires.

Dans cette étude, nous avons choisi d’utiliser les WN pour la modélisation. Il a été prouvé que les WN ont le même pouvoir de modélisation que les RdPC de base (abréviation des RdP P/T) et que tous les modèles construits avec les RdPC de base peuvent être transformés en WN (Chiola et al., 1991). Cela implique que les WN ont un pouvoir de modélisation au moins aussi important que les RdPC abréviation des RdP Places/Transitions.

Sur la partie droite de la Figure 2, nous illustrons les méthodes d'analyse applicables aux modèles WN. L’intérêt de cette classe de RdPC est qu’elle propose des règles de réductions applicables en amont de l’analyse aux modèles initiaux (Haddad, 1991). Toutefois, l’applicabilité de certaines règles de réduction nécessite de valider des conditions d’applicabilité, exigeant ainsi le calcul d’invariants colorés (Couvreur & Martínez 1991). Les propriétés des modèles WN peuvent être évaluées soient par calcul des invariants colorés, soit en construisant un graphe d'accessibilité symbolique (Chiola et al., 1991) qui peuvent réduire considérablement la taille du graphe d’accessibilité.

4 Réseaux de Petri Colorés Bien Formés Les RdPC Bien Formés (Well-Formed Petri Nets, WN) sont une classe de RdPC qui respecte un

certain nombre de contraintes de syntaxe. En raison de la limitation du nombre de pages, nous ne rappellerons ici que les principales caractéristiques des WN. Une définition formelle complète peut être trouvée dans (Diaz, 2009).

Domaines de couleurs des WN Un domaine de couleur des WN est un produit cartésien de classes de couleurs élémentaires qui sont

des ensembles finis et non vides. Une classe de couleur élémentaire peut être ordonnée ou non. Elle caractérise des éléments partageant une caractéristique de même type. Elle peut être partagée en sous-classes statiques, qui permettent de spécialiser cette caractéristique en définissant des sous-ensembles d’éléments ayant potentiellement un comportement similaire (opérations batch, symétries, …). Une couleur neutre (notée ε) est aussi considérée comme une couleur élémentaire pour définir des places et transitions non colorées.

Fonctions de couleurs des WN Dans WN, les fonctions de couleurs sont des sommes pondérées de t-uplets de fonctions de couleur

élémentaires et peuvent être gardées. Il existe trois fonctions de couleur élémentaires : la fonction identité, la fonction de diffusion et la fonction successeur. Soit 𝐶" une classe de couleur et 𝐶 =𝐶$$×𝐶$

&' ⋯ 𝐶)$×𝐶)&* un domaine de couleur. ∀𝑐 =< 𝑐$$,⋯ , 𝑐$

&', ⋯ , 𝑐)$,⋯ , 𝑐)&* > , les fonctions de

couleur élémentaires sont définies par : La fonction identité 𝑋"

1 𝑐 = 𝑐"1 (pour tout 1 ≤ 𝑖 ≤ 𝑘 et 1 ≤ 𝑗 ≤ 𝑒" ). Elle est une projection qui

sélectionne un élément d'un n-uplet. Dans les cas les plus courants où 𝐶 est la couleur d’une transition, les fonctions identités peuvent être remplacées par des variables typées (e.g., 𝑋 et 𝑌 dans la Figure 3).

Figure 3 : Exemple de functions de couleur (soit X=2 et Y=a)


5

La fonction successeur ⨁𝑋"1 𝑐 envoie le successeur de 𝑐"

1 dans une classe ordonnée 𝐶". Elle est aussi notée ⨁𝑌 ou (𝑌 + 1) après le remplacement de la fonction identité 𝑋"

1 𝑐 par une variable 𝑌. La fonction de diffusion est définie par 𝐴𝑙𝑙@A 𝑐 = 𝑥C∈@A et aussi noté 𝐴𝑙𝑙(𝐶") , qui renvoie

l’ensemble des couleurs d'une classe et peut aussi s’appliquer à une sous-classe statique. Gardes Les gardes des WN sont associées à certaines transitions et aussi à certaines fonctions d’incidence.

Les gardes sont des expressions logiques construites à l’aide des opérateurs booléens (∧,∨, 𝑒𝑡¬) appliqués à des prédicats standards. Un prédicat standard peut être l’égalité de deux variables ([X = Y]), ou peut comparer une variable avec le successeur d’une autre variable ([𝑋 =⊕ 𝑌]), ou encore peut être la restriction des valeurs d’une variable à une sous-classe statique D ([X ∈ D]).

Les restrictions précédentes donnent aux WN de bonnes caractéristiques qui permettent de faciliter leur analyse. Les fonctions élémentaires définies permettent de caractériser les symétries du système modélisé. Toutefois, les comportements asymétriques différenciant certains objets d’une classe donnée peuvent être modélisés, à l’aide de la définition de sous-classes statiques et des gardes associées aux transitions ou aux arcs. Ces caractéristiques renforcent le pouvoir de modélisation des WN.

Dans ce travail nous utilisons CPN Tools en nous restreignant à la syntaxe de WN.

5 Motifs de modélisation en WN pour le contrôle automatique des trains

Dans la section 3, nous avons expliqué l’avantage de modéliser un système ferroviaire à l’aide des WN. D’un point de vue pratique, nous avons besoin de modéliser certaines structures de données ou traitement qui ne sont pas intuitifs à l’aide des WN. Nous proposons aussi dans cette section, trois motifs de modélisation (patterns) permettant d’avoir une modélisation systématique et rigoureuse basée sur les WN, pour les systèmes ferroviaires. Ils sont : une structure alternative en WN équivalente aux arcs « if-then-else » définis dans CPN Tools (Jensen et al., 2007) ; la définition d’une fonction successeur ; et la définition de la structure de données « liste » et de ses opérations de gestion correspondantes (ajout d’une cellule, suppression d’une cellule, modification d’une cellule).

5.1 Arcs conditionnels en WN Les arcs conditionnels de type « if-then-else », constituent une structure alternative commune qui

facilite la modélisation de certaines fonctions du système. Ils sont pris en charge par certains outils de RdPC comme CPN Tools, mais, ils ne sont pas implémentés en WN. Dans cette section, nous proposons deux solutions équivalentes basées sur le concept de fonctions gardées ou celui de transitions gardées.

Notations Etant donné un arc associé à la transition t et à la place p, et dont les ensembles de couleurs

respectives sont ∁ t et ∁ p , nous notons WNOPQ 𝑝, 𝑡 la fonction d’incidence de l’arc postérieur de t avec 𝑝 ∈ 𝑡• (et respectivement, WNTé 𝑝, 𝑡 la fonction d’incidence sur l’arc antérieur de t avec 𝑝 ∈ 𝑡• ). Nous définissons une expression conditionnelle « if-then-else » pour cet arc en question :

WNOPQ 𝑝, 𝑡 = 𝑖𝑓𝑔𝑡ℎ𝑒𝑛𝐹[𝑒𝑙𝑠𝑒F^ Où 𝑔 est une condition définie sur ∁ t ; 𝐹[ et 𝐹_ sont deux fonctions colorées non gardées de

couleur ∁(𝑡) sur ∁(𝑝). Proposition 1 : Arcs conditionnels par fonctions gardées. Comme l’expression de 𝑊abc[ 𝑝, 𝑡 n’est pas supportée par la syntaxe des WN, nous définissons

une fonction équivalente 𝑊dabc[ 𝑝, 𝑡 par :


6

𝑊dNOPQ 𝑝, 𝑡 = g 𝐹[ + ¬𝑔 𝐹_

𝑊dabc[ 𝑝, 𝑡 est une somme de t-uplets gardés et donc respecte la définition des fonctions de couleur

gardée de WN (Diaz 2009). Elle possède la même sémantique que l’expression𝑊abc[ 𝑝, 𝑡 . Certains outils RdPC ne prennent pas en charge le concept de fonction gardée. Dans ce cas, il est

possible de modéliser un arc conditionnel en utilisant deux transitions gardées. L’une des transitions modéliserait respectivement la partie « then » et l’autre transition modéliserait la partie « else » de la structure alternative de l’arc conditionnel.

Proposition 2 : Arcs conditionnels par transitions gardées. La proposition 2 sera basée sur les mêmes notations données précédemment, avec G le garde de la

transition t comme illustré par l’exemple dans la Figure 4a. Il est possible que G=TRUE, i.e. que la transition t n’ait initialement pas de garde.

Figure 4 : Cas d’illustration de l’interprétation d’un arc conditionnel par des transitions gardées

L’idée est de remplacer la transition t par les deux transitions 𝑡f et 𝑡g, en définissant ainsi un réseau bien formé équivalent 𝑊𝑁′ = (𝑃j, 𝑇j, ∁j,𝑊NOPQ,𝑊NTé, Φj), avec : - 𝑃j = 𝑃; 𝑇j = 𝑇 ∖ 𝑡 ∪ {𝑡f, 𝑡g}; - ∁j(𝑡f) = ∁j(𝑡g) = ∁(t) ; ∀𝑠 ∈ 𝑃j ∪ 𝑇j ∖ 𝑡f, 𝑡g , ∁j 𝑠 = ∁ 𝑠 ; - 𝑊abc[r 𝑝, 𝑡f = 𝐹[, 𝑊abc[r 𝑝, 𝑡g = 𝐹_, 𝑊asér 𝑝, 𝑡f = 𝑊asér 𝑝, 𝑡g = 𝑊NTé 𝑝, 𝑡 ; - ∀𝑝j ≠ p ∈ 𝑃j, 𝑊∗r 𝑝j, 𝑡f = 𝑊∗r 𝑝j, 𝑡g = 𝑊∗ 𝑝j, 𝑡 où ∗∈ {𝑝𝑜𝑠𝑡, 𝑝𝑟é}; - ∀𝑡j ∈ 𝑇j ∖ 𝑡f, 𝑡g , ∀𝑝j ∈ 𝑃j,𝑊∗r 𝑝j, 𝑡j = 𝑊∗ 𝑝j, 𝑡j où ∗∈ {𝑝𝑜𝑠𝑡, 𝑝𝑟é}; - Φj 𝑡f = G⋀g, Φj 𝑡g = G⋀¬g; ∀𝑡j ∈ 𝑇j ∖ 𝑡f, 𝑡g , Φj 𝑡j = Φ(𝑡j);

Un exemple du réseau bien formé équivalant à la Figure 4a est donné par la Figure 4b. Remarque : Les proposition 1 et 2 sont basées sur un arc avec sa fonction WNOPQ 𝑝, 𝑡 . La

proposition analogue est faite pour un arc avec la fonction Wasé 𝑝, 𝑡

5.2 Fonction prédécesseur Dans les WN, la fonction successeur ⊕𝑋"

1 est définie comme une fonction élémentaire. Dans certains cas de modélisation, il est également nécessaire d’utiliser une fonction prédécesseur. Mais une telle fonction n’est pas définie dans les WN. Nous proposons de définir cette fonction prédécesseur à l’aide des fonctions élémentaires existantes et sous certaines contraintes. Elle sera notée ⊝𝑋"

1. Proposition 3 : Définition d’une fonction prédécesseur. Soit ⊝𝑋"

1(𝑐) une application de 𝑐 ∈ 𝐶 = 𝐶$&'×⋯×𝐶)

&* vers le prédécesseur de la couleur 𝑐"1 dans

une classe ordonnée 𝐶" . Elle est aussi notée ⊝𝑋 ou (𝑋 − 1) après le remplacement de la fonction identité 𝑋"

1 𝑐 par une variable 𝑋. Il convient de noter que le prédécesseur du premier objet de 𝐶" est le dernier objet.

Contraintes d’application : Pour que le RdPC avec la fonction prédécesseur reste un WN, pour chaque < 𝑖, 𝑗 >, si la fonction prédécesseur ⊝𝑋"

1 est utilisée, la fonction successeur correspondante

𝑡

𝑝2

𝑝1

𝑝

𝑊&'() 𝑝, 𝑡 = 𝑖𝑓𝑔𝑡ℎ𝑒𝑛𝐹)𝑒𝑙𝑠𝑒F7

[𝐺] 𝑡;

𝑡<

𝑝1

𝑝

𝑝2

𝑊&'()= 𝑝, 𝑡< = F7

[𝐺⋀𝑔]

[𝐺⋀¬𝑔]

(a) (b)

𝑊&'()= 𝑝, 𝑡; = F@


7

⨁𝑋"1 ne peut pas être utilisée dans le « contexte de la même transition t ». Le « contexte d’une transition

t » comprend les arcs connectés à la transition t ainsi que le garde de cette transition t. En d’autres termes, on ne peut pas utiliser les fonctions prédécesseur et successeur pour la même fonction identité 𝑋"1 dans le même « contexte de transition ».

Pour bénéficier des fonctionnalités de WN, lors de l’analyse d’un réseau coloré utilisant des fonctions prédécesseurs définies par la Proposition 3, on pourrait le transformer en un WN équivalent.

La Figure 5 montre un exemple de réseau coloré utilisant une fonction prédécesseur (Figure 5a) et son équivalent WN (Figure 5b). Dans l’exemple𝐶 𝑡 = 𝐶 = 𝐶1×𝐶1, 𝑋 = 𝑋$$ et 𝑌 = 𝑋$| sont deux fonctions identités; (𝑋 − 1) et (𝑋 + 1) sont les notations de fonction prédécesseur et successeur.

Pour que la fonction prédécesseur (𝑋 − 1) soit remplacée par une structure respectant la règle de WN, nous procédons selon les deux étapes suivantes :

Etape 1 : Rechercher toutes les instances de la fonction d’identification 𝑋 dans le « contexte de la transition t » et les remplacer par la fonction successeur correspondante (𝑋 + 1). Dans l'exemple illustratif, la fonction d’identification 𝑋 dans le garde de la transition t est remplacée par (𝑋 + 1).

Etape 2 : Remplacer toutes les instances de la fonction prédécesseur (𝑋 − 1) par le variable 𝑋. Dans l'exemple illustratif, la fonction prédécesseur (𝑋 − 1) utilisée dans l’arc postérieur de la transition t est remplacée par 𝑋.

Figure 5 : Modèle avec fonction prédécesseur et son équivalent en WN

5.3 Modélisation d’une liste en WN Pour modéliser la fonction autorisation de mouvement, nous avons besoin de modéliser des listes

de circulation. Cette section propose une solution générique pour modéliser et gérer les listes en WN. En prenant l’exemple de la liste de circulation, les déclarations de base sont définies comme suit :

La classe de couleurs POS est ordonnée et est divisée en trois sous-classes statiques. Chaque position dans <1, 2, ..., N> représente un canton de la ligne ferroviaire (qui compte N cantons, N étant par conséquent un paramètre caractérisant chaque ligne réelle). Les deux autres sous-classes statiques <0> et <END> sont réservées à des fins spéciales qui seront expliquées dans la suite de cette partie. « END » représente la valeur N+1 que nous assimilons à un canton virtuel de fin de ligne.

La classe de couleurs TID énumère les identifiants des différents trains pouvant circuler sur cette ligne. T(0) est une valeur réservée qui ne représente pas une circulation réelle. Elle est utilisée pour la gestion de liste. La classe TID est une classe non ordonnée.

Le domaine de couleur TRAINITEM est un produit cartésien 3-uplet POS * TID * POS (Figure 6). Le premier champ (Position_Courante : POS) définit la dernière position connue d’un train, le second donne son identifiant et le 3ème indique le canton occupé par celui qui le précède sur la ligne (Position_Prédécesseur : POS).

Figure 6 : Structure d'un TRAINITEM

Cl = {1..5}

(a) (b)

p1

C1

p2

C1

p3

C1xC1

t

[X=Y]X

Y

( (X-1),Y )p1

C1

p2

C1

p3

C1xC1

t

[(X+1) = Y]X+1

Y

(X,Y)

PositionCourante Identitédutrain PositionduTrainPrécédent

POS TID POS

Classe

Type

CLASS POS = <0>∪<1, 2, …, N>∪<END>; TID = < T(0), T(1), T(2), … , T(M) >; DOMAIN TRAINITEM = <POS, TID, POS>.


8

Pour construire une liste, nous définissions un pointeur de tête de liste et une cellule sentinelle caractérisant la fin de la liste :

Tête de la liste : Elle ne définit pas une circulation réelle, mais sert à référencer la position de la dernière circulation à s’être engagée sur la ligne ferroviaire. Les premier et deuxième champs de la cellule de tête de liste sont toujours "0 : POS" et "T(0) : TID". Son troisième champ indique la position de la dernière circulation, i.e. celle du premier train qui serait rencontré en parcourant la ligne du début vers la fin. Il convient de noter que le canton "0 : POS" n'est pas un canton réel, et que T(0) n’est pas un train réel. Ces valeurs servent à définir la cellule de tête de la liste.

Sentinelle (dernière cellule) : Nous définissions une cellule sentinelle afin de marquer la fin de la liste. Cette cellule modélise la première circulation d’une ligne (c’est-à-dire, parmi les trains présents sur la ligne, elle représente le train ayant commencé à la parcourir en premier). Elle n’a pas de prédécesseur. Pour l’indiquer, nous donnons à son 3ème champ « Position_Prédécesseur » la valeur « END : POS ».

En WN nous modélisons la liste des trains par une place que nous nommerons TrainList et qui est de type TRAINITEM. Chaque jeton coloré dans cette place représente donc une cellule de la liste, c’est-à-dire une circulation sur cette ligne (excepté la cellule de tête). Lorsque la ligne est vide, la place est initialisée avec le jeton <0 : POS, T(0) : TID, END : POS> qui modélise que toute la ligne (de la position 0 précédent le premier canton à la position END, située après le dernier canton N), est affectée au train « virtuel » T(0).

Pour spécifier en WN les opérations sur la liste, nous considérons une deuxième place : la place FreeBlocks qui est de type POS. Elle modélise à un instant donné l’ensemble des cantons non occupés par une circulation. Chaque fois qu’une circulation change de canton, l’identifiant du nouveau canton occupé est retiré de cette place, et celui du canton libéré est remis dans la place.

Afin de présenter la modélisation des différentes opérations en WN, nous considérons l’exemple d’une liste constituée par trois trains comme illustré par la Figure 7.

Figure 7 : Illustration conceptuelle d’une liste de trois circulations

Opération 1 : Insertion d’un nouveau train dans la liste Compte tenu de l’hypothèse 1 (cf. §2.3), cette opération correspond toujours à un ajout en tête de

liste. Pour modéliser cette opération, il est nécessaire de définir la place NewTrain de type TID*POS définissant l’identifiant de la nouvelle circulation à insérer et sa position. La position d’insertion de chaque nouvelle circulation est la valeur 1. Dans la place NewTrain, le jeton à insérer est de type <TrainID = tr: TID, PositionCourante = 1: POS> (Figure 8a) avec ‘tr’, l’identifiant de cette circulation.

Figure 8 : Opération d’insertion en tête (a) et opération de suppression de la queue de liste (b)

L’opération est modélisée par la transition InsertTrain. Dans la place TrainList on récupère le jeton modélisant la tête de liste (<0, T(0), p0> avec ‘p0’ la position connue de la dernière circulation insérée sur la ligne) et dans la place FreeBlocks, on vérifie que le canton 1 est libre. Si oui, on retire le canton de la place Freeblocks et on génère dans Trainslist un jeton tête de liste modifié (<0, T(0), 1>) et un jeton caractérisant la cellule de la nouvelle circulation ajoutée (<1, tr, p0>).

0:POS(tête)

T(0):TID(tête)

2:POS

(DernierTrain)

2:POS

(DernierTrain)

T(1):TID

(DernierTrain)

5:POS(Train

adjacent)

5:POS

(2e Train)

T(2):TID

(2e Train)

9:POS(Train

adjacent)

9:POS

(1er Train)

T(3):TID

(1er Train)

END:POS

(1er Train)

Pointeurversledernier train 2e TrainDernierTrain 1er Train

(b)(a)

FreeBlocks

POS

TrainEND

TrainItem

PassedTrain

TIDxPOS

RemoveTrain

N

(p1, t1, END)

1`(N, tr, END)++1`(p1, t1, N)(tr, N)

FreeBlocks

POS

TrainList

TrainItem

NewTrain

TIDxPOS

InsertTrain

1 1`(0,T(0),1)++1`(1,tr,p0)

(0,T(0),p0)

(tr,1)


9

Opération 2 : Suppression de la première circulation de la liste Quand une circulation arrive dans le dernier canton et quitte la ligne ferroviaire, son jeton <N : POS,

tr: TID, END: POS> doit être retiré de la place TrainList et, le canton <N: POS> doit être libéré. Le jeton correspondant est donc remis dans la place FreeBlocks. Pour caractériser les circulations quittant la ligne, on doit indiquer leur identifiant et leur position sur le dernier canton, en mettant un jeton dans la place PassedTrain qui est de type TID*POS. La Figure 8b montre que les deux jetons représentant la première circulation <N, tr, END> et celle qui la suit sur la ligne <p1, t1, N> doivent être traités dans ce cas. Le franchissement de la transition RemoveTrain supprime le jeton <N, tr, END> et modifie le jeton <p1, t1, N> pour passer son 3ème champ « Position_Prédécesseur » à la valeur "END : POS".

Opération 3 : Mise à jour de la position d’un train La mise à jour de la position d’une circulation (Figure 9) n'affecte pas la relation d'ordre des

circulations dans la liste (cf. hypothèse 1 dans §2.3). De ce fait, elle nécessite la modification de la valeur de deux jetons de la liste des circulations. La demande de modification est faite par la mise d’un jeton dans la place T2RBC, donnant la position courante et l’identifiant de la circulation (<tr, p>). La transition Update1 va retirer de la place Trainlist le jeton de même identifiant que la circulation (<p0, tr, p_pre>) et le remplacer par le jeton (<p, tr, p_pre>). De même elle va retirer le canton p de la place FreeBlocks et y mettre le canton nouvellement libérer p0. Dans un deuxième temps, il est nécessaire de modifier la cellule de la circulation précédant de celle considérée. Cela est fait par le tir de la transition Update2. Son déclenchement est effectué par la mise d’un jeton dans la place OldPos lors du franchissement de l’Update1. Cela entraine la récupération dans la place TrainList du jeton ayant p0 comme valeur du champ « Position_Prédécesseur ». Cette valeur p0 est alors modifiée en p par le franchissement de l’Update2 et un compte-rendu de mise à jour (tr, p) est généré en plaçant un jeton dans la place RBC2T modélisant l’interface avec le train.

Figure 9 : Mise à jour de la position d’une circulation

6 Cas d’étude illustratif Pour construire les contrôleurs discrets d’un système ferroviaire, il est nécessaire de prendre en

compte deux points de vue : un point de vue structurel et un point de vue fonctionnel. Cela nous amène à proposer dans cette partie, trois modèles répondant au point de vue structurel : un modèle de l’architecture du système ferroviaire ; un modèle générique de contrôleur de train ; et un modèle générique de contrôleur de RBC. Les deux modèles génériques de composants du système ferroviaire sont eux même normalement structurés d’un point de vue fonctionnel. Ici, nous proposons des modèles correspondant à la fonction autorisation de mouvement à bord (modèle du train) et au sol (modèle du RBC). Ces modèles sont basés sur les WN et utilisent les motifs de modélisation présentés dans la section précédente.

FreeBlocks

POS

TrainList

TrainItem

T2RBC

TIDxPOS

OldPos

TIDxPOSxPOS

RBC2T

TID

Update1 Update2

(p0,tr,p_pre)

(tr,p) (tr,p0,p)

(p1,t1,p0)(p1,t1,p)

(tr,p0,p)

[p<>p0]p

[p<>p0]p0 (p,tr,p_pre)

(tr,p)


10

6.1 Le modèle structurel de l’architecture La Figure 10 correspond au modèle structurel du système ferroviaire. Ce modèle est construit de

manière modulaire et hiérarchique. Les rectangles aux bordures à double ligne sont des modules au sens de CPN, ils représentent les différents composants du système ferroviaire : les trains et les RBCs, qui sont précisés dans les sections 6.2 et 6.3. Conformément à l’hypothèse 2 (cf. §2.3), nous associons un module RBC à chaque ligne ferroviaire. Les détails du module RBC seront donnés à la section 6.3. Deux modules de train sont ajoutés dans cette vue globale de l’architecture du système.

Figure 10 : Modèle structurel de l’étude de cas

Au niveau architectural, nous distinguons deux types de places : les places d’interface inter-modules et les places d’indentification de chaque module. Les places Train2RBC et RBC2Train modélisent les interfaces sans fil entre les trains et le module RBC. Les jetons sont des messages échangés entre les différents modules. De manière similaire, les places T1Balise et T2Balise modélisent les interfaces des trains avec les Eurobalises. Dans notre étude, les Eurobalises sont utilisées pour informer les trains de leurs positions et des modules de simulation sont donc ajoutés pour générer les séquences des messages nécessaires.

Les places T1ID et T2ID définissent les identifiants respectifs de chaque train. Des arcs bidirectionnels sont utilisés car les jetons d'identifiants ne doivent jamais être consommés ou modifiés. Cela peut également être fait pour les modules RBC, en cas de prise en compte de plusieurs RBCs dans l’architecture d’un système.

Étant donné que tous les modules de trains sont exactement identiques (à l'exception de leurs TID en tant que marquages initiaux), il est possible d'ajouter plus de modules de trains au modèle architectural, à condition de connecter chaque module de trains aux places interfaces et de leur attribuer leurs TIDs.

6.2 Le modèle d’un train La Figure 11 définit le modèle WN d’un train pour parcourir une ligne ferroviaire en utilisant la

fonction autorisation de mouvement. Nous supposons qu’initialement une circulation relative à un train donné arrive sur le premier canton de la ligne considérée. A partir de l’état initial, défini par le marquage (place Balise : 1, place Position : vide, place EOA : 1, place Registered : false), nous décrivons de manière logique, les opérations et les changements d'états permettant de mettre en œuvre la fonction autorisation de mouvement à bord d’un train.

La transition Register est utilisée pour enregistrer le train auprès du RBC. Pour franchir cette transition, le train doit être localisé sur le canton 1 (le jeton “1 : POS” dans la place Balise) et le jeton

Train2RBC

TypexTIDxPOS

RBC2Train

TIDxPOS

T2ID

TID T(2)

T1ID

TIDT(1)

Train2

TrainTrain

Train1

TrainTrain

RBC

RBCRBC

T1Balise

TIDxPOS

T2BaliseTIDxPOS

FreeBlocks

POS

TrainQueueTrainItem

Request

TID

RBC22TOut

TIDxPOSOut

T2RBCIn

TypexTIDxPOS

In

OldPos

TIDxPOS

InsertTrain

RemoveTrain

QueryEOA1

[p_pre=HEAD]

Update1 Update2

QueryEOA2

[!(eoa=N)]

1`1

1`(0,T(0),1)++1`(1,tr,p0)

(1,tr,p0)

N (p1,t1,HEAD)1`(N,tr,HEAD)++1`(p1,t1,N)

(pos, tr, p_pre)

tr

(tr,N)

1`(p,tr,p_pre)

(INSERT,tr,1)

(REMOVE,tr,N)

(UPDATE,tr,p) (tr,p0)

(p1,t1,p0)

(p1,t1,p)

tr(tr,p0)

[!(p=p0)]p[!(p=p0)]p0

(p0,tr,p_pre)

tr

(pos, tr, eoa+1)

tr (tr,eoa)

Position

POS

EOA

POSTrainIn/Out TIDIn/Out

T2RBCOut

TypexTIDxPOSOut

RBC2TIn

TIDxPOS

In

BaliseIn

TIDxPOS

1`(T(1),1)

In

Registered

BOOL

1`false

Advance

[pos<>1]

Receive

Disconnect

Register

pos

tid

eoa

(UPDATE,tid,tpos)

(tid,neoa)

neoa

p0

tid

tid

tid

N

1

(REMOVE,tid,N)

(INSERT,tid,1)

(tid,pos)

false

true

false

true

true

(tid,1)

Position

POS

EOA


T2RBCOut

TypexTIDxPOSOut

RBC2TIn

TIDxPOS

In

BaliseIn

TIDxPOS

1`(T(1),1)

In

Registered

BOOL

1`false

Advance

[pos<>1]

Receive

Disconnect

Register

pos

tid

eoa

(UPDATE,tid,tpos)

(tid,neoa)

neoa

p0

tid

tid

tid

N

1

(REMOVE,tid,N)

(INSERT,tid,1)

(tid,pos)

false

true

false

true

true

(tid,1)

La séquencedesmessagesparbalises

La séquencedesmessagesparbalises


11

de la place Registered doit être « false ». Lorsque la transition Register est franchie, elle met un jeton "1 : POS" dans la place Position et, elle place un jeton de type "INSERT" dans la place d’interface avec le RBC, elle modifie le jeton de la place Registered à « true ».

La transition Advance permet de simuler l'avancement d'une circulation de canton en canton. La circulation avance tant qu’elle n’est pas arrivée à son EOA. Chaque fois que la circulation franchit un canton, elle reçoit de la place Eurobalise la notification de sa nouvelle position. Cela permet un nouveau franchissement de la transition Advance. Le jeton dans la place Position est alors mis à jour, et un rapport de positionnement est envoyé par le train pour informer le RBC de sa nouvelle position.

Figure 11 : Fonction autorisation de mouvement d’un train

La transition Receive est franchissable seulement lorsqu’un message MA a été émis par le RBC pour la circulation considérée. Ce message est mis par le RBC dans la place d’interface RBC2T partagée par tous les trains, mais le message contient l’identifiant de la circulation (tid) auquel est destiné ce MA. Ainsi, seule la transition Receive du module de train correspondant peut être franchie. Après réception du message, la nouvelle valeur de l’EOA de cette circulation est ensuite mémorisée dans la place EOA.

La transition Disconnect sert à informer le RBC quand la circulation a quitté la ligne ferroviaire. Après avoir passé le dernier canton (canton N), cette transition est déclenchée. Cela entraine la suppression du jeton "N : POS" de la place Position. Le module du train envoie un message de type "REMOVE" au RBC et modifie le jeton de la place Registered à « false » indiquant qu’il n’est plus connecté à un RBC.

6.3 Le modèle d’un RBC La Figure 12 représente le modèle d’un RBC avec ses quatre opérations principales : InsertTrain,

RemoveTrain, PositionUpdate (Update1 et Update2) et GenerateEOA (QueryEOA1 et QueryEOA2). Les trois premières opérations correspondent aux trois opérations sur une liste présentée dans §5.3.

L’opération GenerateEOA modélise la réponse du RBC à une demande de MA. La fabrication de la réponse étant variable en fonction de la position de la circulation sur la ligne (en tête de ligne ou autre), nous utilisons la solution de la proposition 2 sur les arcs conditionnels modélisés par transition gardées (Figure 4b). Ainsi l’opération est modélisée par les deux transitions QueryEOA1 et QueryEOA2, et les arcs qui les lient aux places TrainList, Request et RBC2T. L’opération est déclenchée par la réception d’un jeton dans la place Request.

Le déclenchement de ces quatre opérations dépend des messages reçus par le RBC. Les messages sont typés à l’aide d’un champ « Type » indiquant le traitement demandé au RBC. Ce champ prend l’une des valeurs suivantes : INSERT, REMOVE ou UPDATE.

Position

POS

EOA


T2RBCOut

TypexTIDxPOSOut

RBC2TIn

TIDxPOS

In

BaliseIn

TIDxPOSIn

Registered

BOOL

1`false

Advance

[pos<>1]

Receive

Disconnect

Register

pos

tid

eoa

(UPDATE,tid,tpos)

(tid,neoa)

neoa

p0

tid

tid

tid

N

1

(REMOVE,tid,N)

(INSERT,tid,1)

(tid,pos)

false

true

false

true

true

(tid,1)

1`(T(1),1)


12

Figure 12 : Fonction autorisation de mouvement d’un RBC

7 Conclusions et perspectives Dans cet article, nous avons montré qu'il est possible d'utiliser les WN pour modéliser des systèmes

complexes tels que les systèmes ferroviaires, en se basant sur les motifs de modélisation et les techniques que nous proposons. Les motifs proposés permettent de modéliser en WN des structures de données et des extensions d'autres types de réseaux de Petri colorés tels que les CPN définis dans (Jensen, 81). Nous avons illustré nos propositions, en les appliquant à la modélisation de la fonction autorisation de mouvement de système ferroviaire dans le contexte d’ERTMS/ECTS-2.

Les perspectives de ce travail sont de poursuivre la modélisation d'autres fonctions de systèmes ferroviaires, en vue d’une automatisation complète. Nous pensons en particulier à la fonction de routage des trains à l'intérieur d'un nœud ferroviaire. De nos jours, elle est mise en œuvre en mode semi-automatique nécessitant une coopération homme-machine.

Au-delà de la phase de modélisation, il faudra compléter ce travail par l'élaboration d'une méthode permettant la vérification formelle de nos modèles, tout en contrôlant leur explosion combinatoire. Notre objectif est d’utiliser autant que possible des techniques d’analyse formelle. L’idée est, d’une part, de réduire les modèles WN et, d’autre part, de les analyser autant que possible (en nous appuyant directement sur le calcul d’invariants colorés des modèles réduits). Toutefois, nous n’excluons pas non plus de vérifier des propriétés sur le graphe d'accessibilité symbolique. Toutes ces méthodes seront mises en œuvre dans un cadre de vérification modulaire basée sur une approche de type « assume-guarantee reasoning » (Nguyen 2013), qui permet de garantir qu’un modèle global vérifie des propriétés qui ont été vérifiées séparément sur chacun de ses composants.

Remerciements Ce travail a été réalisé dans le cadre d’ELSAT2020, programme de recherche cofinancé par l’Union Européenne avec le Fonds européen de développement régional, par l’Etat et la Région Hauts de France.

Références van der Aalst, W.M.P., Stahl, C. & Westergaard, M., 2013. Strategies for Modeling Complex Processes

Using Colored Petri Nets. In K. Jensen et al., eds. Transactions on Petri Nets and Other Models of Concurrency VII. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 6–55.

FreeBlocks

POS

TrainListTrainItem

Request

TID

RBC22TOut

TIDxPOS

T2RBCIn

TypexTIDxPOS

In

OldPos

TIDxPOS

InsertTrain

RemoveTrain

QueryEOA1

[np=END]

Update1 Update2

QueryEOA21`1

1`(0,T(0),1)++1`(1,tr,p0)

(1,tr,p0)

N (p1,t1,END)1`(N,tr,END)++1`(p1,t1,N)

(pos, tr, np)

tr

(tr,N)

1`(p,tr,np)

(INSERT,tr,1)

(REMOVE,tr,N)

(UPDATE,tr,p) (tr,p0)

(p1,t1,p0)

(p1,t1,p)

tr(tr,p0)

[!(p=p0)]p[!(p=p0)]p0

(p0,tr,np)

tr

(pos, tr, eoa+1)

tr (tr,eoa)

[!(eoa=N)]

Out


13

Berthelot, G. & Lri-Iie, 1986. Checking properties of nets using transformations. In G. Rozenberg, ed. Advances in Petri Nets 1985. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 19–40.

Chiola, G. et al., 1991. On Well-Formed Coloured Nets and Their Symbolic Reachability Graph. In High-level Petri Nets SE - 13. Springer, pp. 373–396.

Couvreur, J.M. & Martínez, J., 1991. Linear invariants in commutative high level nets. In G. Rozenberg, ed. Advances in Petri Nets 1990. Springer Berlin Heidelberg, pp. 146–164.

Diaz, M., 2009. Petri Nets: Fundamental Models, Verification and Applications. London, UK: John Wiley & Sons.

Esparza, J. & Hoffmann, P., 2016. Reduction Rules for Colored Workflow Nets. In Fundamental Approaches to Software Engineering: 19th International Conference (FASE 2016). pp. 342–358.

Haddad, S., 1991. A Reduction Theory for Coloured Nets. In K. Jensen & G. Rozenberg, eds. High-level Petri Nets: Theory and Application. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 399–425.

Janczura, C.W., 1999. Modelling and Analysis of Railway Network Control Logic using Coloured Petri Nets. University of South Australia.

Jansen, L., Meyer zu Hörste, M. & Schnieder, E., 1998. Technical Issues in Modelling the European Train Control System (ETCS) Using Coloured Petri Nets and the Design/CPN Tools. In K. Jensen, ed. Workshop on Practical Use of Coloured Petri Nets and Design. Daimi PB-532, Aarhus, Denmark: Aarhus University, pp. 103–115.

Jensen, K., 1981. Coloured Petri Nets and the Invariant-Method. Theoretical Computer Science, 14(3), pp.317–336.

Jensen, K., Kristensen, L.M. & Wells, L., 2007. Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer, 9(3–4), pp.213–254.

Meyer zu Hörste, M., 1999. Modelling and Simulation of Train Control Systems Using Petri Nets. In FMRail Workshop.

Murata, T., 1989. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, 77(4), pp.541–580.

Ratzer, A.V. et al., 2003. CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets. In Proceedings of the 24th international conference on Applications and theory of Petri nets (ICATPN’03). pp. 450–462.

UNISIG, 2008. ERTMS/ETCS System Requirement Specification (SUBSET-026) V3.0.0 http://www.era.europa.eu/Document-Register/Pages/SUBSET-026v300.aspx

Vanit-Anunchai, S., 2014. Experience using Coloured Petri Nets to Model Railway Interlocking Tables. In 2nd French Singaporean Workshop on Formal Methods and Applications (FSFMA’2014). Singapore, pp. 17–28.

Vanit-Anunchai, S., 2010. Modelling Railway Interlocking Tables Using Coloured Petri Nets. In D. Clarke & G. Agha, eds. Coordination Models and Languages: 12th International Conference (COORDINATION’2010). Amsterdam, The Netherlands, pp. 137–151.

Vanit-Anunchai, S., 2009. Verification of Railway Interlocking Tables using Coloured. In The 10th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. DAIMI PB 590, Department of Computer Science, University of Aarhus, pp. 139–158.

Nguyen, H. V., 2013. Modular Verification of Petri nets. Rapport de master, Université de Bordeaux 1. Xie, Y., Khlif-bouassida, M. & Toguyeni, A., 2016. Modeling of Automatic Train Operation Control

using Colored Petri Nets. In 11th International Conference on Modeling, Optimization & Simulation (MOSIM 2016). Montréal, Canada.

Žarnay, M., 2004. Use of Petri Net for Modelling of Traffic in Railway Stations. In Proceedings of international conference Infotrans 2004.


14

Documents

Modèles Génériques en Réseaux de Petri Bien Formés pour le … · aux concepteurs des briques de modélisation et, d’autre part, de pouvoir exploiter les différentes techniques