30 mars 2017
Présentation vie de groupe, présentation de Pascale Marangé et document de cadrage du GdR MACS.
Modeling and conflicts management for performance evaluation of a public transportation system in (max, +) algebra
Présentation (pdf)
Yassine Idel Mahjoub (1), Ahmed Nait-Sidi-Moh (2), El houcine Chakir El-Alaoui (1)
(1) Laboratoire des Systèmes Electriques et Télécommunications, Université de Cadi Ayyad -FST, Marrakech, Maroc
(2) Laboratoires de Technologies Innovantes, Université de Picardie Jules Verne - INSSET, Saint Quentin, France
This presentation deals with the modeling, analysis and performance evaluation of a public transportation network characterized by choice phenomena, synchronization and concurrency using two complementary formalisms Petri Nets (PN) and (max, +) algebra. We mainly focused on conflicts management and resource sharing within this network in order to evaluate some passengers metrics using (max, +) equations. We are fundamentally interested in evaluating times of arrival, boarding, disembarking and waiting times of each passenger at any network station. Furthermore, we study the influence of the limited capacity of transportation means on passengers travel time. The objective is to find an optimal threshold from which the transportation means capacity has no longer impact on passengers waiting time especially during rush hours.
Diagnostic et Diagnosticabilité des Systèmes à Evénements Discrets Complexes Modélisés par des Réseaux de Petri Labellisés
Présentation (pdf)
Ben Li (École Centrale de Lille, Cristal)
Cette présentation porte sur le diagnostic des systèmes à événements discrets modélisés par des Réseaux de Petri labellisés (RdP-L). Les problèmes de diagnostic monolithique et de diagnostic modulaire sont abordés. Des contributions sont proposées pour résoudre les problèmes d'explosion combinatoire et de complexité de calcul.
Dans le cadre de l'analyse de la diagnosticabilité monolithique, certaines règles de réduction sont proposées comme un complément pour la plupart des techniques existantes de l'analyse de la diagnosticabilité, qui simplifient le modèle RdP-L tout en préservant sa propriété de diagnosticabilité. Pour un RdP-L sauf et vivant, une nouvelle condition suffisante pour la diagnosticabilité est proposée. Pour un RdR-L borné et non bloquant après l'occurrence d'une faute, l'analyse à-la-volée est améliorée en utilisant la notion d'explications minimales qui permettent de compacter l'espace d'état ; et en utilisant des T-semiflots pour trouver rapidement un cycle indéterminé. Une analyse à-la-volée utilisant Verifier Nets (VN) est proposée pour analyser à la fois les RdP-L bornés et non-bornés, ce qui permet d'obtenir un compromis entre efficacité du calcul et limitation des explosions combinatoires.
Dans le cadre de l'analyse de la diagnosticabilité modulaire, une nouvelle approche est proposée pour les RdP-Ls décomposés. Les règles de réduction, qui préservent la propriété de la diagnosticabilité modulaire, sont appliquées pour simplifier le modèle initial. La diagnosticabilité locale est analysée en construisant le VN et le Graphe d'Accessibilité Modifié (MAG) du modèle local. La diagnosticabilité modulaire est vérifiée en construisant la composition parallèle du MAG et des graphes d'accessibilités d'autres modules du système. La complexité de calcul est inférieure à celles des autre approches dans la littérature. D'autre part, l'explosion combinatoire est également réduite en utilisant la technique de ε-réduction.
Décomposition en modélisation et en vérification
Présentation (pdf)
Rim Saddem, Olivier Naud, Karen Godary Dejean et Didier Crestani
Unités de recherche : ITAP & LIRMM
Les systèmes automatisés mobiles, tels que les robots ou les machines pour l'agriculture de précision, peuvent être conçus pour effectuer des actions qui varient dans l'espace en fonction des informations provenant des capteurs ou d'une carte de mission. Pour être fiable, le processus de conception de tels systèmes doit impliquer la vérification combinée des propriétés spatiales et dynamiques.
Nous nous intéresserons dans cet exposé à la modélisation du comportement d'un robot mobile en utilisant l’outil uppaal et à la vérification des propriétés d’atteignabilité qui incluent la recherche de chemin. L'espace est modélisé comme une grille 2D et le chemin du robot mobile n'est pas connu a priori. Plus particulièrement, nous étudierons la vérification d’une propriété d’atteignabilité, que nous appelons « atteignabilité totale bord à bord ».
L'exploration exhaustive de l'espace d'état par l’algorithme du Model checking conduit à la génération de nombreux mouvements possibles. Ceci provoque l’explosion combinatoire. Dans cet exposé, nous proposons une méthodologie de décomposition réduisant les exigences de mémoire pour la tâche de vérification. La décomposition est double. La grille est décomposée en deux sous-grilles et la requête de vérification de modèle sur la grille entière est décomposée en deux requêtes sur les deux sous-grilles. Nous produisons un ensemble de cas de test et nous vérifions la validité du concept de décomposition. La méthode de décomposition est comparée à une méthode plus simple qui vérifie la propriété étudiée sans procéder à la décomposition. Les résultats expérimentaux montrent que la méthode proposée a des meilleures performances par rapport à la méthode simple.
En perspective, une extension de la décomposition en plus de deux divisions sur la grille initiale sera proposée.