Site menu:



              Résumés des exposés

Démarche de conception sure de la supervision de la fonction conduite autonome
Romain Cuer, Laurent Pietrac, Eric Niel, Saidou Diallo, Nicoleta Minoiu-Enache et Christophe Dang-Van-Nhan

Le véhicule autonome est conçu pour se conduire sans aucune intervention du conducteur. Ce véhicule comprend une nouvelle fonction, appelée fonction AD (pour Autonomous Driving), en charge de la conduite lorsque ceci est autorisé. Cette fonction peut se trouver dans différents états (off, disponible par exemple) qui sont gérés par une sous-fonction nommée supervision. Le principal objet de cette étude est de garantir que la supervision d'une fonction, réalisée par un système automobile embarqué critique du point de vue de la sûreté, respecte les exigences fonctionnelles et de sécurité qui lui sont allouées. Puisque deux aspects différents sont étudiés, la mise en cohérence de l'ensemble de ces exigences, dès le début de la conception, est un défi majeur. Dans cet article, une méthode est proposée pour contribuer à résoudre ce problème. Les exigences traitées sont progressivement consolidées en utilisant des modèles comportementaux formels. Les potentielles ambiguïtés, incohérences ou incomplétudes sont ainsi graduellement traitées. De plus, l'application de la méthode à la conception de la fonction AD souligne son efficacité et son intérêt dans un contexte industriel.


Invariance par retour d'état sur le demi-anneau max-plus
Carolina Cardenas, Jean Jacques Loiseau et Claude Martinez

Le concept d'invariance contrôlée est fondamental pour la conception de lois de commande pour les systèmes linéaires soumis à des contraintes définies en termes d'espaces vectoriels. Nous traitons ici de l'extension de cette méthode au cas de systèmes max-plus linéaires, suivant en cela de nombreuses publications récentes. Nous montrons que, dans ce cas également, l'invariance contrôlée équivaut à l'invariance par retour d'état statique. Cela renforce la connexion, qui avait déjà été notée, entre le concept d'invariance et la conception de lois de commande, pour une classe de réseaux de Petri temporisés. Contrairement au cas de systèmes sur un corps, le retour d'état qui rend invariant un demi-module invariant contrôlé n'est pas linéaire, en général. Par contre un tel retour d'état est calculable, en utilisant les solutions connues de systèmes d'équations linéaires dans l'algèbre max-plus. Une autre différence d'avec le cas de systèmes sur un corps est que la causalité du feedback doit être vérifiée, pour permettre sa mise en oeuvre. Nous définissons le concept d'invariance contrôlée causale, et donnons des conditions nécessaires et suffisantes pour qu’un module donné ait cette propriété. Cela ouvre la voie au calcul de solutions optimales à nombre de problèmes de commande pour cette classe de systèmes. Nous l'illustrons sur un exemple tiré de la littérature.


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 et Armand Toguyéni

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.


Contribution à la déterminisation des automates max-plus
Sébastien Lahaye, Aiwen Lai et Jan Komenda

Tous les automates max-plus ne peuvent pas être déterminisés, c'est-à-dire transformés en un automate max-plus déterministe ayant le même comportement. Une généralisation aux automates max-plus de la procédure classique de séquentialisation a malgré tout été intensivement étudiée et celle-ci aboutit pour des sous-classes importantes. Cette procédure utilise une condition sur la normalisation des vecteurs d'état pour détecter et fusionner les états à partir desquels le comportement est semblable. Dans cette contribution, on identifie une nouvelle condition, moins forte, garantissant cette propriété. Cela permet d'améliorer la procédure de déterminisation, si bien qu'elle termine pour une classe plus large d'automates max-plus.


Détection et localisation de fautes temporelles dans les systèmes (max,+)-linéaires
Euriell Le Corronc, Alexandre Sahuguède et Yannick Pencolé

L'automatisation du diagnostic de pannes dans les systèmes industriels tels que les systèmes manufacturiers ou de transport souvent modélisés par des Systèmes à Evénements Discrets (SED) est un enjeu majeur. Il est nécessaire de déterminer rapidement les problèmes sur les équipements afin de les réparer au plus tôt et ainsi maximiser le temps opérationnel et productif du système. Parmi les différents types de pannes, les pertes de performances temporelles sont régulièrement rencontrées comme par exemple une baisse du taux de production de pièces dans un système d'assemblage ou encore un ralentissement de convoyeurs dans un réseau de transport de bagages dans un aéroport. Ces problèmes ne sont pas facilement modélisable avec les méthodes de diagnostic à base de modèles à événements discrets connues à ce jour si bien que les outils classiques de diagnostic ne sont a priori pas bien adaptés pour en déterminer la ou les causes.
L'objectif de cet article est de proposer une méthode de détection et de localisation de fautes temporelles pour une classe de SED temporisés appelés systèmes (max,+)-linéaires. Ce type de système permettant la représentation de phénomènes de synchronisation entre ressources, de durées d'opération et de temps de transmission est particulièrement bien adapté pour identifier des décalages temporels non souhaités typiques des problèmes dans les procédés industriels.
La méthode proposée se déroule en plusieurs étapes. A partir d'un flux d'observations temporisées, le problème consiste tout d'abord à déterminer si ce flux résulte d'un comportement en présence d'une faute temporelle ou non. Des indicateurs de fautes sont utilisés pour répondre à cette question et reposent sur l'utilisation de la théorie de la résiduation appliquée aux systèmes (max,+)-linéaires. Si la faute est détectée, il est alors nécessaire de la localiser au mieux dans le système. Les fautes temporelles potentielles sont donc répertoriées et ajoutées au modèle (max,+) du système en comportement normal. Ensuite, de manière analogue à la théorie classique du diagnostic dans les systèmes à temps continu, des matrices de signatures sont proposées et permettent de déterminer les fautes candidates expliquant les observations.


Analyse des Réseaux de Petri Temporels Exécutés de Manière Synchrone
Ibrahim Merzoug, Karen Godary-Dejean et David Andreu

Lors de la conception de systèmes numériques complexes, le recours aux méthodes formelles est utile notamment pour valider les propriétés du système, avec certitude. Cependant, les processus de validation usuels font abstraction des propriétés non fonctionnelles, notamment celles issues des contraintes d'exécution sur la cible matérielle. En l'occurrence, l'analyse des réseaux de Petri temporels doit être étudiée avec attention lorsque ce formalisme, intrinsèquement asynchrone, est exécuté de façon synchrone sur un FPGA. Il faut alors considérer la synchronisation d'horloge, le parallélisme effectif et l'interprétation. Actuellement, aucune sémantique formelle et aucune méthode d'analyse ne s'attaquent à toutes ces problématiques en même temps. Ainsi, nous proposons une nouvelle méthode d'analyse pour les réseaux de Petri interprétés exécutés en synchrone, avec une sémantique formelle d'exécution et un graphe d'états spécifique : le Graphe de Comportement Synchrone.


Évaluation de la robustesse d'un ordonnancement par Automates Temporisés Stochastiques
Sara Himmiche, Pascale Marangé, Alexis Aubry, Marie Duflot et Jean-François Pétin

Les modèles et outils des Systèmes à Evénéments Discrets (SED) ont montré leur apport et leur efficacité pour la modélisation et la résolution de problèmes d'ordonnancement dans le domaine des systèmes manufacturiers de production. Leur principal atout réside dans leur capacité à appréhender naturellement les dynamiques sous-jacentes aux ressources de production ainsi que les logiques de configuration des ateliers (Job-shop, Flow-shop, Open-shop, hybrides...).
De plus, les extensions stochastiques des modèles de SED offrent d'intéressantes perspectives pour la prise en compte de l'incertain en ordonnancement : incertitudes sur les ressources (durée opératoires, aléas de fonctionnement, pannes...) mais aussi sur la demande (variabilité importante des produits, personnalisation de masse...). L'objectif de cet article est de démontrer la faisabilité d'une approche basée sur les automates temporisés stochastiques et sur des techniques de model-checking statistique pour ́évaluer la robustesse d'un ordonnancement face à des aléas en se restreignant, dans le cadre de cette ́étude, aux incertitudes sur les durées opératoires.


Diagnostic de motifs de comportements dans les systèmes temporels
Yannick Pencolé et Audine Subias

Dans cet article nous proposons une formulation du problème de diagnostic de motifs d'un système temporel. Il s'agit de rechercher à partir d'une séquence d’observations du système, toutes les évolutions de celui-ci qui non seulement produisent la séquence observée mais aussi qui sont concordantes avec les motifs d'intérêt considérés. La caractérisation formelle du problème de diagnostic s'appuie sur la notion de pattern matching (concordance de motifs). Posé sous forme d’un problème d'atteignabilité, le problème de diagnostic est résolu par model checking.


Diagnostic et contrôle de la dégradation des systèmes probabilistes
Nathalie Bertrand, Serge Haddad et Engel Lefaucheux

Le diagnostic actif est opéré par un contrôleur en vue de rendre un système diagnosticable. Afin d'éviter que le contrôleur ne dégrade trop fortement le système, on lui affecte généralement un second objectif en termes de qualité de service. Dans le cadre des systèmes probabilistes, une spécification possible consiste à assurer une probabilité positive qu'une exécution infinie soit correcte, ce qu'on appelle le diagnostic actif sûr. Nous introduisons ici deux spécifications alternatives. La gamma-correction du système affecte à une exécution une valeur de correction dépendant d'un facteur de décote gamma et le contrôleur doit assurer une valeur moyenne supérieure à un seuil fixé. La alpha-dégradation requiert qu'asymptotiquement, à chaque unité de temps une proportion supérieure à alpha des exécutions jusqu'alors correctes le demeure. D'un point de vue sémantique, nous explicitons des liens significatifs entre les différentes notions. Algorithmiquement, nous établissons la frontière entre décidabilité et indécidabilité des problèmes et dans le cas positif nous exhibons leur complexité précise ainsi qu'une synthèse, potentiellement à mémoire infinie.


Diagnosticabilité des Systèmes à Evènements Discrets : Une Nouvelle Variante de l'Approche Diagnostiqueur
Abderraouf Boussif et Mohamed Ghazel

Dans ce papier, nous nous intéressons à l'analyse de la diagnosticabilité des systèmes à évènements discrets modélisés par des automates à états finis. En particulier, une variante de l'approche diagnostiqueur initiée par Sampath et co. [1, 2] est présentée. Cette variante repose sur une nouvelle structure qui consiste à séparer explicitement les états normaux de ceux fautifs à l'intérieur de chaque nœud du diagnostiqueur. Une telle distinction permet de suivre séparément l'évolution des traces normales et fautives dans le diagnostiqueur. Différentes caractéristiques de la nouvelle structure sont ensuite exploitées pour (i) raffiner la condition nécessaire et suffisante de la diagnosticabilité [1], (ii) développer une nouvelle condition nécessaire vérifiable directement sur le diagnostiqueur sans revenir au modèle, (iii) proposer une version simplifiée de la condition nécessaire et suffisante, et enfin (iv) développer une procédure systématique pour l'analyse de la diagnosticabilité basée sur un algorithme de vérification à la volée. L'évaluation de cette approche est faite à travers une série d'expérimentations et de comparaisons avec des approches classiques de référence.


Approche originale utilisant le Raisonnement à Partir de Cas pour le Diagnostic en Ligne des Systèmes Automatisés de Production
Nourhène Ben Rabah, Ramla Saddem, Faten Ben Hmida, Véronique Carré-Menetrier et Moncef Tagina

Ce papier s'inscrit dans le cadre du diagnostic en ligne des Systèmes Automatisés de Production (SAP) classés ici dans les Systèmes à Evénement Discret (SED). Il présente une approche originale utilisant le raisonnement à partir de cas (RàPC). L'originalité de cette proposition réside dans les quatre items suivants : (1) elle utilise ce type de raisonnement pour le diagnostic de cette catégorie de systèmes, (2) elle propose un format de représentation de cas inspiré du formalisme Signatures Temporelles Causales (STC) qui s'adapte à l'aspect dynamique des systèmes à surveiller, (3) elle expose une phase qui couple simulation et mise en forme de données pour la transformation des données issues du système simulé après son émulation en mode normal et défaillant, et (4) elle présente une phase de raisonnement et d'apprentissage qui permet non seulement le diagnostic en ligne du système surveillé mais aussi la mise à jour de la base de cas suite à l'apparition de nouveaux comportements inconnus.


Parametric Analyses of Concurrent Systems : Vérification paramétrée temporisée et probabiliste
Etienne André, Benoît Delahaye, Didier Lime et Olivier H. Roux

La vérification formelle, et notamment la vérification de modèles (model-checking), permet de garantir la correction du modèle d'un système par l'exploration exhaustive de tous ses comportements.
Le model-checking a acquis une certaine reconnaissance académique, mais son applicabilité en pratique reste toutefois un peu décevante. Ceci est dû en partie à deux problèmes : une modélisation un peu rigide au détriment de la capacité d'abstraction et du passage à l'échelle, ainsi qu'un retour d'information insuffisant lors de la vérification. La vérification paramétrée permet de lever en partie ces restrictions, en considérant le problème plus général suivant : « pour quelles valeurs des paramètres le modèle est-il conforme à sa spécification ? ». Dans cet exposé, nous présentons deux formalismes paramétrés avec deux types de paramètres : les automates temporisés paramétrés (où les paramètres représentent des valeurs temporelles) et les chaînes de Markov à intervalles paramétrés (où les paramètres représentent des valeurs de probabilités).


Session posters / démonstrateurs
GT SED (Sébastien Lahaye et Laurent Piétrac) et GT AFSEC (Claude Jard, Claire Pagetti et Olivier H. Roux)

Organisée par les groupes SED (Systèmes à Evénements Discrets) et AFSEC (Approches Formelles des Systèmes Embarqués Communicants), cette session a pour objectif de présenter à la communauté les travaux en cours et les outils logiciels développés ou utilisés dans le cadre de travaux de recherche relatifs à la modélisation, l'analyse et la commande des systèmes réactifs et temps réel.

TABS : un outil logiciel d'ordonnancement de la production basé sur les automates temporisés
Rémi Pannequin, Pascale Marangé, Alexis Aubry et Jean-François Petin

SEDMA - un outil pour la Modélisation, l'Analyse et la génération automatique de programme pour les SEDs
Romain Pichard, Michel Combacau, Alexandre Philippot, Ramla Saddem et Bernard Riera

MinMaxGDJS - Calcul dans le semi-anneau MinMax[[gamma,delta]]
Mehdi Lhommeau, Laurent Hardouin et Bertrand Cottenceau

Identification de systèmes réactifs
Jérémie Saives, Gregory Faraut et Jean-Jacques Lesage

IMITATOR: vérification de systèmes temps-réel concurrents en présence d'incertitude
Étienne André

Modeling and Simulation of Air France Baggage-Handling System with Colored Petri Nets
Dina L. Hafilah, Andi Cakravastia, Younsse Lafdail et Naly Rakoto

MaxplusPy : librairie Python de calcul dans l'algèbre max-plus et de manipulation d'automates à multiplicités
Sébastien Lahaye

Evaluation de performances des automates temporisés avec gardes en utilisant l'algèbre (Max,+) - Application aux systèmes de commande en réseau
Ferhat Tamssaouet et Saïd Amari

Démonstrateur ASSecIN: ligne industrielle virtuelle permettant l'évaluation de passerelle intelligente
Thomas Toublanc, Sébastien Guillet, Florent Frizon De Lamotte et Pascal Berruet

DIAG-IPF: A Software Tool for Fault Diagnosis of Discrete Event Systems
Abderraouf Boussif et Mohamed Ghazel




Modélisation et évaluation de performances d'un réseau de bus basées sur les réseaux de Petri colorés et l'algèbre (max, +)
Yassine Idel Mahjoub, Ahmed Nait-Sidi-Moh et El Houcine Chakir El-Alaoui

Dans cet article, nous nous sommes focalisés sur l'étude d'un réseau de bus régi par différents phénomènes dont la synchronisation, le parallélisme et les situations de conflits. Une nouvelle approche de modélisation des systèmes de transport public basée sur les réseaux de Petri colorés et l'algèbre (max, +) est proposée. L'objectif est de combiner ces deux outils pour modéliser, analyser et évaluer les performances d'un réseau de bus tout en remédiant au problème de l'explosion combinatoire. Plus précisément, nous nous intéressons à l'évaluation des tableaux de marches des différents bus ainsi que les dates de montée et de descente de chaque passager aux différentes stations. Par ailleurs, l'influence de la capacité supposée finie des bus sur les temps d'attente des passagers sera aussi ́etudiée et analysée. De façon plus générale, cette étude peut être appliquée à n'importe quel réseau de transport public de n'importe quelle taille.


Vérification formelle des programmes automates de la SNCF par model-checking
Mohamed Niang, Alexandre Philippot, François Gellot, Raphael Coupat, Bernard Riera et Sébastien Lefebvre

Suite à l'ouverture du marché, le Réseau Ferré National (RFN) français doit faire face à la concurrence du transport ferroviaire européen. Afin de garder sa position de leader du marché ferroviaire français, la Société Nationale des Chemins de Fer français (SNCF) cherche à mettre en place des solutions innovantes permettant d'améliorer la sécurité et les conditions de travail de ses chargés d'études lors des travaux d'automatisation. Partant de l'étude théorique d'un projet jusqu'à sa validation sur site, les chargés d'études doivent effectuer un certain nombre de tâches qui s'avèrent souvent être longues, complexes et répétitives, ce qui a pour effet d'augmenter leurs charges de travail. Ce projet de recherche se focalise principalement sur une des tâches les plus importantes, qui est la vérification des programmes automates (aspects fonctionnels et sécuritaires). L'objectif est d'améliorer la méthodologie de vérification des programmes automates en mettant en place un outil qui permettra aux chargés d'études d'effectuer cette tâche de manière efficace et automatique.


Un langage graphique pour la modélisation et l’analyse des systèmes réactifs
Hamzat Olanrewaju Aliyu, Oumar Maïga et Mamadou Kaba Traoré

Une étude exhaustive d'un système complexe nécessite souvent l'utilisation de plusieurs méthodes d'analyse (comme la simulation, l'analyse formelle, ou l'émulation) pour produire des réponses complémentaires aux questions qui se posent. La combinaison de multiples méthodes d'analyse offre plus de possibilités et de rigueur pour analyser un système que ne peut le faire chacune des méthodes prise individuellement. Si cet exercice permet d'aller vers une connaissance complète des systèmes complexes, son adoption pratique ne va pas de pair avec les avancées théoriques en matière de formalismes. Ce déficit rend nécessaire la lourde tâche de créer et de gérer plusieurs modèles du même système dans différents formalismes et pour différents types d'analyse. Nous proposons, dans cette communication, de réduire cette tâche à la spécification d'un modèle unique duquel pourront être conduites des analyses multiples, grâce à un langage graphique de haut niveau permettant de fédérer la simulation, l'analyse formelle et l'émulation.


DPN-SOG: A Software Tool for Fault Diagnosis of Labeled Petri Nets Using the Semi-Symbolic Diagnoser
Abderraouf Boussif, Mohamed Ghazel et Kais Klai

In this paper, we present DPN-SOG, a software tool written in C++ for fault diagnosis of discrete event systems modeled by bounded labeled Petri nets. DPN-SOG (for Diagnosability analysis of Petri Nets using Symbolic Observation Graphs) implements the semi-symbolic diagnoser approach developed in [1, 2] for fault diagnosis of bounded labeled Petri nets. The implemented approach aims to cope with some limitations of the classic diagnoser-based approaches, namely the state-space explosion problem, the intermediate models and the double-checking procedure for diagnosability analysis. The key features of DPN-SOG are: (i) the on-the-fly building of the diagnoser and analysis of diagnosability, (ii) the generation of only the necessary part of the diagnoser to perform the diagnosability analysis and online diagnosis, and (iii) the evaluation of the time/memory consumption for the construction of the diagnoser and the analysis of diagnosability.