Synthèse d'un superviseur ferroviaire à partir d'exigences avec PetriGen

21/10/2017
Publication REE REE 2005-2
OAI : oai:www.see.asso.fr:1301:2005-2:20564
DOI :

Résumé

Synthèse d'un superviseur ferroviaire à partir d'exigences avec PetriGen

Métriques

1
0
1.42 Mo
 application/pdf
bitcache://d10d7e3093ed954a8f6cb53e462b7bbcf94b6b58

Licence

Creative Commons Aucune (Tous droits réservés)
<resource  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
                xmlns="http://datacite.org/schema/kernel-4"
                xsi:schemaLocation="http://datacite.org/schema/kernel-4 http://schema.datacite.org/meta/kernel-4/metadata.xsd">
        <identifier identifierType="DOI">10.23723/1301:2005-2/20564</identifier><creators><creator><creatorName>Thomas Bourdeaud'huy</creatorName></creator><creator><creatorName>Pascal Yim</creatorName></creator></creators><titles>
            <title>Synthèse d'un superviseur ferroviaire à partir d'exigences avec PetriGen</title></titles>
        <publisher>SEE</publisher>
        <publicationYear>2017</publicationYear>
        <resourceType resourceTypeGeneral="Text">Text</resourceType><dates>
	    <date dateType="Created">Sat 21 Oct 2017</date>
	    <date dateType="Updated">Sat 21 Oct 2017</date>
            <date dateType="Submitted">Fri 17 Aug 2018</date>
	</dates>
        <alternateIdentifiers>
	    <alternateIdentifier alternateIdentifierType="bitstream">d10d7e3093ed954a8f6cb53e462b7bbcf94b6b58</alternateIdentifier>
	</alternateIdentifiers>
        <formats>
	    <format>application/pdf</format>
	</formats>
	<version>34736</version>
        <descriptions>
            <description descriptionType="Abstract"></description>
        </descriptions>
    </resource>
.

Dossier LOGISTIQUE ET TRANSPORT (2) Synthèse d'un superviseur m a « ferroviaire à partir d'exigences avec PetriGen Par Thomas BOURDEAUD'HUY, PascalYIM École Centrale de Lille, LAGIS - Villeneuve dascq mronym MLt'H " Synthèse deréseaux dePetri, Synthèse desuperviseurs, Programmation par contraintes, Exigences defonctionnement, Modélisation 1. Introduction La sécurité des systèmes de transport, en particulier ferroviaires, est une préoccupation particulièrement actuelle. Nos recherches sur ce thème s'inscrivent dans un cadre régional (Nord-Pas de Calais), avec le pôle ST2 (Sécurité des transports terrestres), national, avec l'action spécifique CNRS 164 sur l'ingénierie des exigences, et européen avec le réseau d'excellence ferroviaire EURNEX. Nous proposons de fonder la phase de conception du système de contrôle sur la notion d'exigences. Le concept d'exigence est emprunté au domaine de l'ingénierie sys- tème qui traite du développement d'applications logi- cielles complexes, s'étendant des systèmes embarqués ou des produits à base d'informatique embarquée jusqu'à la grande entreprise ou aux systèmes technico-économiques impliquant des ressources informatiques. L'ingénierie des exigences désigne la première étape du développement d'une application logicielle complexe qui consiste à définir clairement les exigences imposées à l'application avant de la concevoir. Par « exigences », on désigne les caractéristiques attendues de l'applica- tion, entendues au sens large : fonctionnalités, perfor- mance, coût, efficacité, sécurité, disponibilité, etc. L'ingénierie système s'est sentie spécifiquement concernée par la notion d'exigences depuis le rapport du « Chaos » du Standish Group en 1994 [11]. Ce rapport met en évidence l'importance de la prise en compte des exigences dans le processus de développement industriel : . Plus des 2/3 du coût final d'un système est défini au moment de la formalisation des exigences ; . Un défaut détecté lors de la phase de spécification est 40 fois moins cher à corriger que s'il avait été détecté durant la phase de validation ; ESSENTIEL SYNOPSIS Dans le cadrede démarchesde type contrôle-commandede sys- tèmes à événementsdiscrets,nousnousintéressonsà l'étape de modélisationpour laquellenous proposons un mécanisme semi- automatique. Nous présentons ainsi dans ce document une démarche et un outil qui permettent la synthèse de réseauxde Petri parcontraintes. Notre démarche s'appuie sur l'utilisation d'un réseau de Petri «partiel» dont la structure est contrainte par un ensemble de spécifications structurelles ou comportementales. Notre outil, PetriGen,est unéditeurde réseauxde Petridoté de fonctionnalités avancées permettant de faciliter ce processus de synthèse. Il permet un interfaçage simple et rapide avec la plupart des solveurs de contraintes,et offre des outils classiquesde visuali- sation,d'édition et de sauvegardedes réseauxgénérés.Soninter- face rédigéeen Tcl/Tklui permet d'être compatibleavec la plupart des systèmesd'exploitation,et facilite le développementde fonc- tionnalitésspécifiquesà chaqueutilisateur.Petrigenpermet aussi l'utilisation de fonctions écrites en langageC pour les traitements réclamant plus de puissance,et rend donc possible l'utilisation des librairiesde résolutionde contraintesles plus courantes. Nous illustrons finalement l'applicabilité de notre démarche sur l'exemple de la synthèse d'un contrôleur ferroviaire. ln this paper,we present a conception methodology based on system requirements,within which we proposeto integratefor- malisationand verification into the same process. This method uses the constraint programming paradigmto synthesize Petri nets correspondingto a formal expression of requirements as constraintsoverthe PNstructure. Someadditionaltechniquesare providedto incrementallyrefine the synthesizednet until it satis- fies the whole requirements. We present also a tool called "PeîrGen", which implements the synthesis methodology, and how it can be usedto synthesizea railway controller. REE N2 Février 2005 Synthèse d'un superviseur ferroviaire à partir d'exigences avec PetriGen . La gestion des exigences est à l'origine de 40 % des facteurs clés de succès d'un projet ; . Une mauvaise gestion des exigences est à l'origine de 48 % des causes d'échecs d'un projet. Depuis lors, quelques outils ont été développés pour la gestion des exigences, par exemple DOORS de Telelogic, qui permet d'assurer la « traçabilité » des exi- gences au fil des phases du développement du système. Cependant, les exigences ne sont pas encore prises en compte dès le début de la phase de spécification, elles interviennent plutôt lors de la phase de vérification. 2. Approches formelles De multiples approches s'intéressent précisément à cette problématique de vérification. Parmi elles, les méthodes formelles semblent les plus pertinentes. Elles consistent à construire une description formelle du système qui sera utilisée pour vérifier que les spécifications ont bien été prises en compte, et que le système considéré restera dans un état sûr durant son fonctionnement. Nous renvoyons le lecteur intéressé aux publications de Clarke et al. [5], Caillaud et al. [4] et Van Lamsweerde [12] pour des références complètes et à jour sur ce que nous consi- dérons comme les trois principales approches formelles au sens large : le model-checking, la synthèse de super- viseurs et les techniques de spécification formelle. Actuellement, chacune propose des mécanismes stables et performants. Certaines ont déjà été utilisées pour des problèmes industriels complexes (par exemple, la méthode de spécification formelle B a été uti- lisée pour valider la ligne de métro à grande vitesse CI METEOR), les autres n'en sont pas loin. Nous proposons quant à nous d'utiliser les réseaux de Petri [8] comme outil de description des systèmes à étudier. Ceux-ci sont déjà utilisés dans chacun des trois domaines précédents. Ils sont à mi-chemin entre les langages formels et les techniques de description transitionnelles : leurs solides fondements mathématiques, ainsi que leurs multiples extensions et sémantiques, permettent de penser qu'ils peu- vent servir à unifier les approches précédentes pour déve- lopper une méthodologie de conception complète. Nous décrivons notre proposition dans le chapitre 3, dans lequel nous associons « exigences » et « réseaux de Petri » pour développer une niéthodologie originale permettant d'intégrer dans une même démarche des tech- niques de formalisation et de vérification. Cette approche est décrite en détails dans [3]. Pour des raisons pratiques évidentes, nous nous limitons aux exigences les plus facilement formalisables, c'est-à-dire aux exigences de fonctionnement : disponibilité, fiabilité, sécurité, sûreté, maintenabilité, tolérance aux fautes, etc. 3. Méthodologie de conception incrémentale Notre méthodologie consiste à synthétiser un réseau de Petri qui fera office de contrôleur pour le système considéré. Puisque notre technique de synthèse se fonde sur l'expression d'exigences, nous proposons ici d'utiliser les techniques de programmation par contraintes. Chaque exigence est exprimée comme une contrainte sur la structure du réseau cherché, et un mécanisme de résolution permet de résoudre les contraintes pour trouver les réseaux les plus pertinents. Nous avons privilégié cet outil de résolution du fait des possibilités d'énumération de solutions qu'il permet. 3.1. Interprétation L'expression formelle des exigences nécessite une connaissance minimale du futur rôle des éléments du réseau à synthétiser. De ce fait, avant de pouvoir formuler les contraintes correspondant aux exigences, une première étape d'interprétation doit être menée. Elle consiste à associer à certains des futurs noeuds du réseau une « signifzcation ». Du fait du grand nombre de réseaux solution potentiels, cette étape permet aussi de définir des bornes pertinentes sur le nombre de places, de transitions et sur les poids des arcs des réseaux à générer. A la fin de cette étape, nous disposons donc d'un réseau de Petri partiel dont le nombre d'éléments (places, transitions) est connu, mais non les arcs reliant ces derniers. 3.2. Formalisation Nous procédons ensuite à la formalisation des exi- gences en termes de contraintes utilisant les éléments « pré-interprétés » lors de l'étape précédente. Une fois les contraintes formulées, un mécanisme de résolution de contraintes peut être mis en route. 3.3. Sélection Lorsque le processus de résolution de contraintes est terminé, un certain nombre de réseaux ont été pro- duits. Il faut alors choisir le « meilleur » représentant parmi les solutions générées, en fonction de critères additionnels. 3.4. Raffinements Puisque certaines exigences ne peuvent pas être exprimées sous forme de contraintes pertinentes - par exemple à cause de considérations portant sur la perfor- mance du mécanisme de résolution de contraintes - la procédure de décision précédente peut être complétée par un processus de raffinement supplémentaire permettant d'intégrer de façon incrémentale un nombre de plus en plus grand de contraintes initialement prévues. Ainsi, le réseau initial produit à l'étape précédente représente en REE No 2 Février 2005 Dossier LOGISTIQUE ET TRANSPORT (2) , .- JI : : -, : j'J ; L,'\ LHi\Î : VI> nl' t il, 41, 1 l, J, '. Figvcre1. Captures d'écran des interfaces de PetriGen. quelque sorte une « classe de contrôleurs » à l'intérieur de laquelle nous cherchons à obtenir un contrôleur qui satisfera finalement l'ensemble des exigences formulées. De façon à illustrer sur un exemple non trivial l'applicabilité de notre approche, nous développerons dans la suite les étapes de la démarche présentée ci-des- sus à travers l'exemple de la synthèse d'un contrôleur ferroviaire. Avant cela, nous commençons par présenter brièvement l'outil PetriGen avec lequel cette expérimen- tation a été menée. 4. L'outil PetriGen PetriGen est une application destinée à outiller les processus de synthèse de réseaux de Petri par la pro- grammation par contraintes Il propose ainsi un ensemble de fonctions pour faciliter la spécification, la synthèse, la visualisation et la simulation de réseaux de Petri. PetriGen a été développé au sein du laboratoire d'au- tomatique, de génie informatique et signal de Lille. Au départ, il s'agissait d'utiliser des algorithmes génétiques pour faire de l'apprentissage de comportements par réseaux de Petri, démarche qui a fait l'objet d'une publi- cation dans [2]. Nous nous sommes depuis orientés vers des algorithmes de programmation par contraintes pour la synthèse de réseaux de Petri, avec en tête la démarche introduite précédemment. PetriGen se compose d'une interface graphique (figure l, à gauche) proposant les fonctions classiques d'édition de réseaux de Petri, et d'un éditeur de texte 1 (figure l, à droite) permettant d'utiliser tout applicatif conforme à la syntaxe Prolog [7]. Son interface rédigée en Tcl/Tk lui permet d'être compatible avec la plupart des systèmes d'exploitation, et facilite le développement defonctionnalités spécifiques à chaque utilisateur. Il per- met aussi l'utilisation de fonctions écrites en langage C pour les traitements réclamant plus de puissance, et rend donc possible l'utilisation des librairies de résolution de contraintes les plus courantes. Le mécanisme de synthèse de réseaux de Petri s'appuie sur le solveur de contraintes Prolog IV. En effet, l'éditeur Prolog intégré permet non seulement d'ouvrir, de sauvegarder et d'éditer un fichier-source Prolog, mais aussi de le compiler et de tester des buts sans sortir de l'application. De cette façon, les exigences sont formali- sées sous forme de prédicats, et une résolution de contraintes permet de générer un réseau qui est ensuite transféré à la partie graphique de l'interface. Ce mécanisme repose sur l'utilisation d'un « canal logique » ouvert entre l'environnement de travail et l'exécutable Prolog. Il suf- fit d'indiquer par l'intermédiaire de l'interface ou d'un fichier de configuration l'exécutable Prolog souhaité et ZD ses options de démarrage. PetriGen est disponible gratuitement à l'adresse : http ://www.ec-lille.fr/tomnab/. Il nous paraît avoir atteint une certaine maturité, et son principe de fonctionnement fondé sur un langage de script, son architecture et sa sou- plesse lui permettent de pouvoir traiter la quasi-totalité des classes de réseaux de Petri et de leurs applications, pour un investissement de développement négligeable. Il est accompagné d'un manuel de 80 pages environ [1], décrivant le logiciel en profondeur. Le lecteur intéressé par une évaluation des autres outils traitant des réseaux de Petri pourra consulter le comparatif disponible sur http ://www.daimi.au.dk/PetriNets/tools/ [Stô981. PetriGen est également référencé sur ce site. REE No 2 Février 2005 Synthèse d'un superviseur ferroviaire à partir d'exigences avec PetnGen N G1 s s \ S-. s. i. ,Ai.i A, 4 \ s) z 21 Figarre2. Réseatiferi-oiiciire à coiitrôler. 5. Synthèse d'un contrôleur ferroviaire Nous souhaitons développer un contrôleur pour le réseau ferroviaire présenté dans la figure 2. Le but de ce contrôleur est de faire circuler deux trains sur des itiné- raires utilisant un tronçon comtnun, de façon que le com- portement contrôlé soit cyclique. L'objectif ultime est de produire un réseau de Petri sauf de façon que le superviseur généré puisse être tra- duit en un grafcet, et implanté le plus directement pos- sible sur les automates de contrôle du réseau ferroviaire considéré. Une synthèse complète permettrait également de tenir compte des caractéristiques particulières de cer- taines sections de voie, qui peuvent être alimentées en continu ou au contraire contrôlées par l'intermédiaire de coupe-circuits, mais nous ne la développerons pas ici. Notre réseau dispose de deux gares Gl et G2 dans les- quelles les trains stationnent initialement. Le réseau est découpé en 5 sections de voie reliées entre elles par deux aiguillages A 1 et A2. Chaque aiguillage peut être com- mandé de façon à se placer en position « directe » ou « bifurquée », suivant la section que l'on souhaite faire emprunter par le train qui y circule. Nous reprenons ci-dessous le découpage présenté plus haut pour présenter les grandes étapes de la synthè- se du contrôleur correspondant. 5.1. Interprétation Nous choisissons d'utiliser 7 places pour chaque train (une place par section et les deux gares) pour indiquer la position courante du train, 5 places pour modéliser la res- source « section de voie » ainsi que 4 places pour désigner la position courante de chaque aiguillage. Nous définissons également 8 transitions par train correspondant aux par- cours prédéfinis de chaque train dans le noeud ferroviaire, et nous relions ces transitions aux places correspondantes. 5.2. Formalisation des exigences Les exigences imposées au contrôleur s'inscrivent dans 2 catégories. Des exigences comportementales qui servent à indiquer quelles sont les séquences d'actions (i.e. les séquences de tirs de transitions) possibles. Des exigences structurelles qui correspondent à des contraintes de sûreté du contrôleur : chaque train ne peut être que dans une section de voie à la fois, une section de voie ne peut contenir qu'un seul train, un aiguillage est dans un état à la fois, etc. Une fois l'ensemble des contraintes formulées dans PetriGen, nous lançons le pro- cessus de résolution permettant la synthèse des réseaux vérifiant l'ensemble des contraintes imposées. 5.3. Sélection, raffinements Nous choisissons parmi les réseaux générés celui qui nous semble le plus apte à être traduit en grafcet, et nous le raffinons de façon à le rendre déterministe en privilégiant - grâce à une place de contrôle [9] - la circulation du train 1 par rapport au train 2. Le contrôleur final obtenu contient 24 places et 16 transitions, il permet aux trains de circuler suivant les trajets définis et garantit - sans avoir à recourir à davantage d'analyse - que le fonctionnement généré est sûr. 6. Conclusion Notre démarche s'est appuyée sur l'utilisation d'un réseau de Petri « partiel » dont la structure est contrainte par un ensemble de spécifications structurelles ou com- portementales. Notre proposition s'est articulée en deux phases successives. D'abord, à partir d'une connaissance minimale de la structure, des propriétés et du comportement désiré du système, un problème de synthèse de réseaux de Petri a été défini. Il a été formulé à l'aide d'un réseau de Petri REE No 2 Février 2005 Dossier LOGISTIQUE ET TRANSPORT (2) N "''t ! f. : - i tl ( l w, si'. Il (1 i S (... 1 1 ' [*, i i il fi (1il (, el. " t il, l %.-4 W rrth ;>r. Iilnrn,r Ii,niu uiW = \) r " i !,, f:u,l A ! (,l i S-% l il fi ; 1- 1 iII7 « : I, fil, iii :,, f'ns'... Figure 3. La méthodologie iiicrénientale proposée. partiel, dont les variables sont contraintes par certaines des exigences précédentes. Le problème correspondant a été résolu en utilisant des techniques de programmation par contraintes. Les résultats ont été ensuite raffinés de façon à prendre en compte progressivement l'ensemble des exi- gences de fonctionnement spécifiées initialement. Nous avons résumé dans la figure 3 l'ensemble des étapes de la démarche proposée. Notre outil, PetriGen, est un éditeur de réseaux de Petri doté de fonctionnalités avancées permettant de faci- liter ce processus de synthèse, grâce notamment à l'inté- gration aisée d'outils de programmation en logique par contraintes de type Prolog. Nous envisageons d'étudier une approche fondée sur la programmation linéaire, de façon à pouvoir utiliser des outils de résolution perfor- mants comme la librairie d'optimisation Cplex. Références [1] T. Bourdeaud'huy., « Pefr/Ger ?, un outil pour la synthèse de réseaux de Petri par la programmation par contraintes. Manuel pour l'utilisateur et le développeur », 81 pages. référencé sur le site Petri nets world, mai 2003. 12l T. Bourdeaud'huy and P. Yim., « Petri net controller synthe- sls using genetic search » (prix du meilleur article étudiant). ln SMC'02, Internatonal Conference on Systems, Man and Cybernetics, Hammamet, Tunisie, 6-9 octobre 2002. [3] T. Bourdeaud'huy and P. Yim., « Synthèse de réseaux de Petri à partir d'exigences » ln MOSIM'04, Conférence francophone de modélisation et simulation, Nantes, France, 1-3 septembre 2004. [4] B. Caillaud, P. Darondeau, L. Lavagno, and X. Xie., « Synthesis and Control of Discrete Event Systems ». Kluvver, 2002. (51 E. M. Clarke, 0. Grumberg and D. A. Peled., « Model Checking ». MIT Press, 2000. [61 A. Cheng., « Petri nets, iraces, and local model checking ». n Algebraic Methodology and Software Technology, 1995. [7] P. Deransart and L. Cervoni, « Pro log : The Standard : Reference Manual ·. Springer Verlag, 1996. [8] M. Diaz et al, « Les réseaux de Petri - Modèles fonda- mentaux » Hermes Science, Traité IC2 Information- Commande-Communication, 2001. [9] A. et al. Giua., « Generalized mutual exclusions constraints on nets wtth uncontrollable transitions ». In Procs. of the IEEE Int. Conf. on Systems, Man and Cybernetics, Chicago, octobre 1992. [101 H. Stbrrle., ( (An evaluation of /-end tools for Petri nets ». Technical report, Ludwlg-Maximilians-Universitat Munich, 1998. [11] Standish Group., « The chaos report (www.standish- group.com/sample-research/chaos-1 994-l.php, 1994 [12] A. Van Lamsweerde., « Formal specification : a roadmap ». ln ICSE - Future of SE Track, pages 147-159, 2000. m ; L e s ; a u t e u r s, 1-1 Thomas Bourdeaud'huy est né à Lille en 1978. Après avoir obtenu son diplôme d'Ingénieur de l'Ecole Centrale de Lille et un DEA d automatique et d'informatique Industtielle en 2001, il s'oriente vers le doctorat d'automatique et d'intormatique. I : obtient en 2004 le grade de docteur de luniver.slté avec un mémoire intitulé Technlques d'abstractlon pour l'analyse el la synthèse de 1 éSeaLIX de Pet i ", sous ! a directioi de Pascal Yim. Pascal Yim est professeur des universités, à l'Ecole Centrale de Lille. Ses travaux de recherche sont basés sur le croisement de concepts Issus de I automatique discrète et de l'IIlformatique, avec Ull Intérêt particulier pour ! es réseaux de Petri, la programmation par contraintes et les systemes d'information. Son domaine d'applica- tion pnncipal concerne la conception et l'optimisation des systèmes de transport, en particulier ferroviaires " Il a publié de nombreux artlcles dans des revues et conférences Internationales. Il a egale- ment supervisé plusieurs contrats industriels (SNCF, port fluvial de Lille, 3 Suisses France.) Pascal Yim anime ie groupe francophone sur les réseaux de PetriIl est responsable d'un thème du pôle régional sur la sécurité des transports terrestres (ST2) et il est correspolldant du réseau d'excel- lence européen sur le ferrcviaire EURNEX. REE No 2 Février 2005