18 mars 2016

Apport des techniques symboliques pour l'analyse de diagnosticabilité des SED modélisés par des réseaux de Petri

Abderraouf Boussif (direceur de thèse : Mohamed Ghazel)

FSTTAR*, Département COSYS - Unité ESTAS, Villeneuve d'Asc

This work discusses the diagnosability analysis of Discrete Event Systmes (DESs) modeled as labeled transition systems, with a focus on Petri nets models. The proposed approach consists in constructing a diagnoser based on the Symbolic Observation Graph (SOG), which combines symbolic and enumarative representations in order to build a determinitic observer from a partialy observed models (automata or Petri nets). The symbolic observation graph was firstly used for the formal verification using event-based model-checking as an efficient alternative to the Kripke structure. Besides, the construction of the diagnoser as well as the verification of diagnosability are performed simultaneously on the fly, which can considerably reduce the generated state-space of the diagnoser and thus the overall running time. To show the effectiveness of symbolic representation in diagnosability analysis, we discuss some experimental and comparative results of the proposed approach relatively to other existing methods based on DES benchmarks.

Distributed Execution of Modular Discrete Controllers for Data Center Management

Présentation (pdf)

Soguy Mak-Karé Gueye (directeur de thèse : Eric Rutten)

Equipe CTRL-A, INRIA Grenoble

Complex computing systems are increasingly designed so that they are self-adaptive, and adopt the autonomic computing approach for their administration. Real systems require the co-existence of multiple such autonomic management loops. Their uncoordinated execution can lead to problematic interferences and jeopardize performance as well as consistency. This is a typical example of the general need for methodological support for the design of well-coordinated managers, without breaking their natural modularity. We address the problem with a method stressing modularity, and focusing on the discrete control of the interactions of managers. We focus on proposals for the distributed execution of modular controllers, first in (partially) synchronized way, and then relaxing this synchronization. We apply and validate our method on a multiple-loop multi-tiers system in a data-center.

Ordonnancement d’ateliers à partir de patrons de modélisation basés sur des automates communicants

Présentation prochainement disponible

Pascale Marangé, Alexis Aubry, Jean-François Pétin

Centre de Recherche en Automatique de Nancy

Cette présentation propose de montrer comment des patrons de modélisation à base d’automates communicants peuvent être utilisés pour l’ordonnancement d’ateliers de type Job-shop/Flow-shop/Open-shop ou hybride. Les approches classiques de recherche opérationnelle et d’optimisation pour résoudre des problèmes d’ordonnancement nécessitent souvent des prérequis importants et le modèle obtenu est très dépendant de l’application. Suite à des premiers travaux ayant montré la pertinence d’une modélisation par automates communicants et de l’obtention d’un ordonnancement réalisable par recherche d’atteignabilité, l’objectif ici est de présenter comment cette approche de modélisation permet à un utilisateur lambda de construire son modèle sans prérequis particulier. L’autre force de cette modélisation réside dans le fait qu’elle ne nécessite pas d’efforts supplémentaires pour passer d’un type d’atelier à un autre ou pour prendre en compte des modifications dans la structure du problème étudié. Cette présentation, après avoir détaillé les patrons de modélisation (machine, opération) et rappelé l’approche d’obtention d’un ordonnancement, présente l’automatisation de l’instanciation de ces modèles à partir d’informations basiques qu’un décideur pourrait connaître. Ceci permet de démontrer que l’approche proposée est générique, simple dans sa modélisation, et évolutive.

Scheduling by Timed Automata under Resource Conflicts

Présentation (pdf)

Mahya Rahimi (directeurs de thèse : Eric Niel, Emil Dumitrescu)

Laboratoire Ampère

Considering time and resource limitations in different industries, increases importance and complexity of task scheduling problems. The main objective of this work is to propose a model and a tool for automatic scheduling of a system with specific set of tasks in order to minimize system’s makespan as much as possible. In this system, resource sharing and multi-resource allocation to each task is considered. Therefore there might be mutual exclusion between tasks in using resources. In addition, it is assumed that all tasks are non-preemptive. As the first step of this research, a new model is proposed and implemented in a tool named UPPAAL 4.1.19 in order to solve aforementioned scheduling problem while considering all tasks to be controllable. For this purpose, following steps are taken: 1. Illustrating resource conflicts through single state (max,+) automata. 2. Translating single state automata to a timed automata model which is compatible with UPPAAL 4.1.19 software. 3. Performing reachability analysis in UPPAAL along with using “fastest diagnostic trace” feature in order to obtain the minimum makespan and one of the fastest trajectories for scheduling. 4. Designing a Gantt chart in UPPAAL to visualize simultaneous execution of tasks. Although this tool can show the optimum trajectory and the desired Gantt chart as visualized outputs, in industrial cases, handling this model with the specific type of timed automata in UPPAAL is complicated; since it requires so many variables to be initialized as inputs. As a future research, this model could be simplified in order to be formalized. Also the model could be extended to consider uncertainty in task duration.