Dates clés

résumés: 15 avril
soumission: 5 juin
notification: 16 juillet
version finale: 12 septembre
posters: 30 septembre
conférence: 18-20 novembre

Contact

msr2015@inria.fr

10ème Colloque sur la Modélisation des Systèmes Réactifs (MSR 2015)

Résumés des exposés

Nathalie Bertrand (exposé invité)
Fault diagnosis for probabilistic systems
Fault diagnosis aims at detecting the occurrence of faulty events in partially observable systems. When it comes to probabilistic models, one can relax the notion of diagnosability by requiring that the set of ambiguous sequences is of null measure. In our talk, we will explain how to solve the following questions: How to check whether a probabilistic system is diagnosable? And in case it is not diagnosable, can one control a system so that it is? For these diagnosability and active diagnosability problems, as well as for the diagnoser synthesis question, we will establish precise complexity bounds.
Quentin Gaudel, Pauline Ribot, Elodie Chanthery
Vers une architecture de surveillance de santé d'un système hybride sous incertitudes
Ces travaux proposent d'effectuer de la surveillance de santé sous incertitudes pour des systèmes hybrides en utilisant une méthode basée sur des modèles. La surveillance de santé s'effectue grâce à des méthodes de diagnostic et de pronostic et nécessite donc un modèle de comportement et un modèle de dégradation du système. Le formalisme des réseaux de Petri hybrides particulaires (HPPN) est défini dans un contexte de surveillance de santé pour générer des diagnostiqueurs de systèmes hybrides. L'avantage principal des HPPN est la manière dont ils gèrent les incertitudes sur la connaissance du système et les observations. Ils modélisent aussi des incertitudes sur les équations du modèle et sur les observations continues en intégrant un filtrage particulaire. Le formalisme prend également en compte la dégradation du système. On utilise ces informations incertaines pour en déduire un résultat de diagnostic sous incertitudes. L'approche est illustrée sur un exemple de système complexe.
Ben Li, Manel Khlif-Bouassida, Armand Toguyéni
Diagnosticabilité de Réseaux de Petri Labellisés basée sur les explications minimales et les T-semiflots
Dans cet article, une approche est développée pour l'analyse de la diagnosticabilité des systèmes à événements discrets (SEDs) modélisés par des Réseaux de Petri Labellisés (RdP-L). L'objectif de ce travail est de combattre l’explosion combinatoire dans l'analyse de la diagnosticabilité à partir d'un modèle RdP-L. Notre approche étend l'analyse à la volée. Elle propose des améliorations basées sur les concepts d'explications minimales et de T-semiflots. Basée sur la recherche en profondeur d'abord, cette approche améliore l'efficacité de l'analyse de diagnosticabilité en construisant l'espace d'état de manière compacte en utilisant le concept d'explications minimales. De plus, cette approche définit des priorités dans le parcours des branches du graphe d'accessibilité à l'aide de T-semiflots. Notre approche a pour objectif de trouver plus rapidement l'existence de cycles indéterminés et de construire l'espace d'état de manière compacte, afin de réduire le coût de mémoire de l'analyse de diagnosticabilité.
Ghyslain Maitre, Yannick Pencolé, Audine Subias and Houssam-Eddine Gougam
Modélisation et Analyse de chroniques pour le diagnostic
Dans cet article nous proposons un modèle de chronique qui peut être vu comme une extension d'un Problème Temporel Simple, permettant d'intégrer dans les chroniques les contraintes d'interdiction représentant l'absence d'un événement dans l'ensemble du comportement modélisé ou sur une partie prédéfinie. Sur la base de cette formalisation nous proposons des critères permettant de caractériser les chroniques et de les comparer afin d'évaluer la pertinence de la base de chroniques utilisée pour le diagnostic. En particulier nous proposons une méthode d'analyse de diagnosticabilité reposant sur un test d'exclusivité des chroniques. Ce test permet de s'assurer que deux chroniques ne peuvent être reconnues par un même flux d'événements généré par le système. Les chroniques sont modélisées par réseaux de Petri temporels et le test d'exclusivité est posé sous forme d'un problème d'atteignabilité et résolu par une méthode de vérification automatique de modèle.
Kabland Toussaint Gautier Tigori, Jean-Luc Béchennec, Olivier Henri Roux
Approche formelle pour la spécialisation de systèmes d'exploitation temps réel
Le développement d'un système d'exploitation spécialisé pour une application consiste, à partir du code d'un système d'exploitation complet, à l'élaguer pour l'adapter aux fonctionnalités nécessaires à l'application. L'opération d'élagage est réalisée à la main au cas par cas. Cela rend très difficile la vérification et la certification d'un système d'exploitation car non seulement la phase de certification est à réaliser pour chaque spécialisation mais aussi le problème difficile et bien connu du fossé entre le modèle utilisé pour la vérification et le code est à étudier au cas par cas. Dans cet article, nous proposons une méthode pour l'automatisation complète de cet élagage au moyen d'une synthèse du système d'exploitation à partir d'un modèle formel embarquant le code du système d'exploitation. Ce modèle comporte en effet à la fois le flot de contrôle, les variables du système d'exploitation et les séquences d'instructions manipulant ces variables. L'élagage, formalisé par l'élimination des chemins infaisables du modèle, permet de ne conserver que la partie accessible (et donc utile) du modèle et donc du code. Cette méthode, non seulement accélère considérablement l'adaptation du système d'exploitation mais, de plus, garantit l'optimalité du code généré et l'absence de code mort. La vérification et la certification de toutes les fonctionnalités souhaitées du système d'exploitation comme l'absence de blocage, peuvent être également réalisées sur le modèle avant la génération de code. Nous utilisons un modèle du système d'exploitation temps réel Trampoline compatible OSEK et AUTOSAR, qui est reconnu comme fiable et largement utilisé aux niveaux académique et industriel.
Sébastien Lahaye, Jan Komenda, Jean-Louis Boimond
Amélioration de la procédure de déterminisation des automates (max,+)
Une classe importante de systèmes à événements discrets peut être modélisée à l'aide d'automates (max,+) et les études utilisant ce formalisme ont notamment contribué à l'évaluation de performances et la commande supervisée de ces systèmes. Pour ces résultats, la propriété de déterminisme des automates manipulés est souvent prépondérante. Or, contrairement aux automates logiques, tous les automates (max,+) ne peuvent pas être déterminisés, c'est-à-dire transformés en un automate (max,+) déterministe ayant le même comportement. Une généralisation aux automates (max,+) de la procédure classique de séquentialisation a tout de même été intensivement étudiée et celle-ci se termine avec succès pour des classes importantes d'automates. Cette procédure utilise une condition sur la normalisation des vecteurs d'état pour détecter et fusionner les états engendrant un identique comportement ultérieur. Dans cette contribution, on identifie une nouvelle condition garantissant cette propriété. Cela nous permet d'enrichir la procédure de déterminisation de sorte qu'elle aboutisse pour une classe plus large d'automates (max,+).
Jean-Louis Colaço (exposé invité)
De LUSTRE à Scade 6
SCADE désigne à la fois un langage de programmation synchrone et l'environnement de développement de logiciels embarqués critiques construit sur ce langage. Initialement conçu comme le pendant graphique du langage LUSTRE, il s'est enrichi de nouveaux traits tout en conservant les fondamentaux du flot de donnée synchrone. Dans cet exposé nous retracerons quelques faits de cette évolution depuis LUSTRE jusqu'à Scade 6 et nous donnerons un état de nos expériences d'extensions du langage pour la modélisation de systèmes hybrides.
Abderraouf Boussif, Mohamed Ghazel
Une Approche par Décomposition de Modèles pour l'Analyse de la Diagnosticabilité des Systèmes à Evènements Discrets par Model-Checking
Cet article s'intéresse à la vérification de la diagnosticabilité des systèmes à évènements discrets (SEDs) dans le contexte de model-checking. Le formalisme de modélisation adopté est les systèmes de transitions labellisés (LTSs). Dans un premier lieu, nous proposons un algorithme permettant la transformation d’un LTS à base d'évènements en un LTS à base d'états, dont le but est d'étendre l'application de l'analyse de la diagnosticabilité par Model-Checking au contexte de diagnostic à base d'évènements. Pour remédier au problème de l'explosion combinatoire de l'espace d'états, nous proposons une technique de décomposition de modèles, qui permet d'extraire uniquement la partie nécessaire pour l'analyse de la diagnosticabilité. L'idée est basée sur la séparation entre les comportements normal et fautif du système. Dans le cas où le système est diagnosticable, nous fournissons une spécification dans la logique temporelle RT-CTL pour analyser la Kmin-diagnosticabilité en un coup, sans faire appel à un processus incrémental. L'évaluation de nos contributions est faite à travers une étude expérimentale effectuée sur un benchmark relatif à un système de contrôle/commande ferroviaire.
Ronan Cossé, Denis Berdjag, Sylvain Piechowiak, David Duvivier, Christian Gaurel
Méthodologie et application du méta-diagnostic de systèmes complexes sur un banc d'intégration avionique
Le nombre de fonctionnalités des systèmes embarqués aéronautiques ne cesse d'augmenter et leur tests deviennent très difficiles à mettre en place. Des erreurs peuvent apparaître lors des phases de validation des logiciels embarqués. Ces tests sont réalisés sur des sous-systèmes appelés bancs d'intégration qui recréent l'environnement réel d'un aéronef. Cependant ces sous-systèmes peuvent également subir des pannes. Cet article propose une méthode pour réaliser leur diagnostic. Cette méthode est mise en place sur le banc d'intégration d'un hélicoptère via le développement d'un logiciel et d'une méthodologie de diagnostic adaptés. Ceci est illustré avec la description d'un problème réel apparu pendant une phase de test.
Nizar Chatti, Rémy Guyonneau, Laurent Hardouin
Diagnostic à base de modèles et aide à la prise de décision robuste par une approche ensembliste
L'un des enjeux les plus importants des technologies impliquées dans l'ingénierie des systèmes complexes concerne aujourd'hui le diagnostic temps réel. Cette discipline repose principalement sur les algorithmes de détection et de localisation de défauts. Dans le présent papier, nous présentons une méthode générique permettant d'améliorer la robustesse de la procédure de détection de défauts. Cette méthode procède en deux étapes distinctes. Dans un premier temps, l'approche des Bond Graphs est utilisée pour générer, sur la base d'un modèle graphique, un ensemble d'indicateurs de défauts appelés résidus. Dans un second temps, les seuils de détectabilité permettant d'évaluer ces résidus sont déterminés grâce à l'analyse par intervalles et aux techniques de satisfaction de contraintes dans le but de réduire au maximum le taux de fausses alarmes et de non détection. Les performances de la méthode proposée sont démontrées par des données expérimentales provenant d'un robot omnidirectionnel.
Jean-Jacques Lesage (exposé invité)
Identification comportementale des Systèmes à Événements Discrets
L'identification est une technique expérimentale qui offre une alternative à la modélisation par connaissance. Elle consiste à rechercher un modèle mathématique d'un système dynamique à partir de la seule observation de son comportement ; elle est dite passive lorsque cette observation est pratiquée pendant le fonctionnement normal du système, qui n'est alors soumis qu'aux sollicitations ambiantes. Dans cet exposé, on s'intéresse à l'identification passive et de type boîte noire des Systèmes à Événements Discrets. Deux approches d'identification sont décrites. L'une permet d'obtenir le modèle identifié sous la forme d'Automates Finis et a été conçue dans l'objectif de produire un modèle sur lequel est basé une approche de diagnostic ; l'autre permet d'obtenir le modèle identifié sous la forme d'un Réseau de Petri Interprété et est dédiée à la rétro-conception.
Adja Ndeye Sylla, Maxime Louvel, François Pacull, Eric Rutten
Génération de règles de coordination à partir de réseaux de Petri colorés
Cet article présente un environnement de génération de règles de coordination à partir de réseaux de Petri colorés. L'environnement proposé est basé sur un langage dédié appelé cpnDSL. À partir d'une spécification cpnDSL décrivant un système donné, des règles de coordination correctes par construction et directement exécutables dans l'environement LINC sont générées. Un modèle vérifiable pour valider le comportement du système et un modèle graphique pour permettre la discussion entre les différents membres du projet sont également générés. Une étude de cas issue du domaine du transport est présentée pour illustrer l'approche proposée.
Laurent Truffet
Comparaison de Chaînes de Bellman par Couplage Croissant
Les chaînes de Bellman-Maslov-Quadrat constituent un exemple de système dynamique autonome sur semi-anneau idempotent fondamental pour l'optimisation.

Dans un premier temps nous étudions le couplage croissant de deux mesures idempotentes (i.e. à valeurs dans un semi-anneau idempotent). Ce couplage peut être vu comme une version idempotente du problème du tableau de contingence de Fréchet à trous. Mais nous le traitons comme un problème de transport de mesures idempotentes à la Monge-Kantorovitch-Hitchcock. La condition nécessaire et suffisante d'existence de couplage croissant est équivalente à la condition de forte dualité dans le problème de transport. Cette condition est la version idempotente de la dominance stochastique d'ordre un. Il s'agit d'un préordre sur les mesures idempotentes. Nous montrons que l'ensemble des probabilités idempotentes muni de ce préordre a une structure de type treillis. Nous donnons les formules closes pour la borne supérieure et la borne inférieure de deux probabilités idempotentes.

Dans un deuxième temps nous caractérisons les opérateurs de Bellman monotones au sens de ce préordre. Pour un opérateur de Bellman donné nous construisons les opérateurs monotones optimaux bornants.

Dans un troisième temps, au titre des applications possibles, nous montrons comment étudier de grandes chaînes de Bellman en combinant monotonie et critère d'agrégation exacte de processus.

Les résultats de ce papier concernent la comparaison de marginales de dimension un de chaîne de Bellman mais l'intérêt d'étudier ce couplage est qu'il permet de comparer des marginales de dimension quelconque. Cet aspect n'est pas développé dans ce travail.

Dimitri Bouche, Jean Bresson
Articulation dynamique de structures temporelles pour l'informatique musicale
Les systèmes informatiques musicaux se divisent principalement en deux catégories: les systèmes de composition en temps différé et les systèmes de performance en temps réel. De récents travaux et applications ont introduit des systèmes se situant à la frontière de ces deux paradigmes, permettant à des processus de calcul statiques de s'intégrer au sein de contextes dynamiques, et inversement. Cela nécessite l'élaboration de techniques mettant en oeuvre des modèles réactifs intégrant des structures temporelles se déroulant sur le long terme, ne permettant pas l'utilisation de stratégies classiques de vision à court terme. Nous introduisons un système établissant une représentation des données musicales de haut niveau (orientée objet), accompagnée d'un moteur d'exécution dynamique bas niveau. Les stratégies de planification purement réactives n'étant pas adaptées aux contraintes musicales de ce système, nous dressons une étude comparative des techniques existantes et proposons un modèle mélangeant mécanismes statiques et dynamiques.
Marc Antoni (exposé invité)
Why do railways need formal specifications and proofs
Frederico Alvares De Oliveira, Eric Rutten, Lionel Seinturier
Modèles comportementaux pour le contrôle de composants logiciels autonomes
Les systèmes logiciels modernes et leur architecture doivent s'adapter dynamiquement de façon réactive aux événements provenant de l'environnement (p. ex. la charge de travail demandée par les utilisateurs, les modifications apportées aux fonctionnalités) et de la plate-forme d'exécution (p. ex. les ressources disponibles). Les architectures à base de composants ont montré leur adéquation pour l'auto-adaptation, non seulement en raison de leurs caractéristiques intrinsèques, comme la réutilisation et la modularité, mais aussi en raison de leurs capacités de reconfiguration dynamique. Cependant, les solutions existantes sont basées souvent sur des langages de bas niveau, impératifs, et sans modèle comportemental. Cet article présente Ctrl-F, un langage dédié pour le support de haut niveau pour la spécification des comportements et des politiques d'adaptation dans les systèmes à base de composants logiciels. Nous nous appuyons sur la programmation réactive pour la vérification et le contrôle des reconfigurations. Nous intégrons Ctrl-F avec FraSCAti, une plate-forme intergicielle pour les architectures réparties orientées services.
Mohamed Escheikh, Bilen Ben Abbes, Ahmed Ameur, Kamel Barkaoui, Hana Jouini
Modélisation et étude de performance de l'équilibrage de charge LTE par ajustement dynamique des paramètres du handover
Nous nous proposons dans cet article d'implémenter par simulation à travers ns-3 des fonctionnalités Self-Organizing Networks (SON) d'auto-optimisation se rapportant à l'équilibrage de charge pour les systèmes radio-cellulaires mobiles LTE. L'implémentation est réalisée au travers deux algorithmes ajustant dynamiquement les paramètres du handover (HO) en se basant sur les mesures de la puissance reçue du signal de référence (RSRP). Cet ajustement est effectué en fonction aussi bien de la charge de la cellule congestionnée que celle des cellules voisines moins chargées et disposées à coopérer pour une meilleure répartition de la charge.

Les résultats numériques obtenus par simulation concernant les deux algorithmes d'équilibrage de charge implémentés et un algorithme étalon de handover (déjà implémenté dans ns-3) basé sur l'évènement A3 mettent en évidence les avantages que procure l'équilibrage de charge en termes de throughput global (dans l'ensemble du réseau), de taux de pertes et de nombre de handovers. Ils montrent aussi les compromis nécessaires entre ces différentes métriques pour aboutir à un équilibrage de charge performant.

Laurent Piétrac, Emil Dumitrescu and Eric Niel
Contribution formelle à l'expression des spécifications pour la conception de contrôleurs discrets
La théorie du contrôle par supervision fournit un cadre formel pour la modélisation des Systèmes à Evénements Discrets (SED) et la synthèse de contrôleurs en fournissant une distinction explicite entre le système non contrôlé et les spécifications. Elle a de nombreuses extensions et applications et a donné lieu à de nombreux travaux de par le monde. L'utilisation des événements comme élément central de l'étude des systèmes est la clé de ce succès.

Elle a cependant l'inconvénient de contraindre le concepteur à étudier la dynamique des systèmes uniquement à travers des successions d'événements. Cela n'est en théorie pas une limite, mais en pratique cela peut rendre difficile l'expression des spécifications. Dans cet article nous proposons un nouveau type d'automate à états facilitant l'expression de ces spécifications tout en restant dans le cadre du contrôle de systèmes modélisés par des automates à états tels qu'utilisés dans la théorie RW.

Bernard Riera, Alexandre Philippot, David Annebicque and François Gellot
La commande par contraintes logiques de sécurité : principe, applications et mise en œuvre
Cet article présente pour la première fois dans son ensemble l'approche de commande par contraintes logiques de sécurité développée au CReSTIC depuis plusieurs années. Le principe consiste à ajouter à la fin du programme API (Automates Programmables Industriels), avant la mise à jour des sorties, un code spécifique (appelé filtre logique) permettant la détection d'une erreur de commande et sa correction (ou compensation). L'approche revient à séparer les aspects fonctionnels et sécuritaires du contrôleur et à considérer un programme API existant comme intervenant uniquement dans la partie fonctionnelle du contrôleur. L'ensemble des contraintes de sécurité est conçu indépendamment du programme API et dépend seulement de la Partie Opérative étudiée. Trois utilisations possibles du filtre logique sont possibles: bloquant, superviseur et contrôleur, permettant entre autres de garantir la sécurité de programmes API existants de façon non intrusive. Les atouts principaux de l'approche sont: la facilité d'implémentation dans un API et son acceptabilité du fait qu'elle peut s'adapter à des programmes existants sans avoir à fondamentalement modifier les méthodes de travail des automaticiens. Les contraintes de sécurité logiques peuvent être vérifiées formellement hors ligne par model-checking. Toutefois, en amont de cette étape lourde de vérification, il est important de s'assurer simplement de la cohérence du filtre logique. Cet article propose à ce titre quelques propriétés nécessaires pour la cohérence des contraintes de sécurité. Un exemple pédagogique virtuel de système manufacturier conçu à partir du logiciel de simulation FACTORY I/O de la société Real Games permet d'illustrer la méthode développée.

Posters

Hamida Bouaziz
Une Approche Incrémentale pour Adapter des Blocs SysML
Hervé Boulet, David Annebicque, Frédéric Nollet, Najib Essounbouli
Contribution à la commande et la supervision intelligentes appliquées à l'efficacité énergétique
Dorina Ionescu, Nicolae Brinzei, Jean-François Pétin
Approche compositionnelle sur les langages probabilistes pour l'évaluation quantitative des séquences d'événements en sûreté de fonctionnement
Pascale Marangé, Alexis Aubry, Jean-François Pétin
Ordonnancement d'ateliers à partir de patrons de modélisation basés sur des automates communicants
Dmitry Morozov, Sergei O. Kuznetsov, Mario Lezoche, Hervé Panetto
Formal methods for process knowledge extraction
Mahya Rahimi, Eric Niel, Emil Dumitrescu
Scheduling by Timed Automata under Resource Conflicts
Jérémie Saives, Gregory Faraut, Jean-Jacques Lesage
Identification comportementale des Systèmes à Evénements Discrets réactifs
Julien Thuillier, Ramdane Tami, David Delouche, Pascal Vrignat, Frédéric Kratz
Caractérisation d'un dysfonctionnement sur un réseau de communication interconnectant un système automatisé