Site menu:



              Résumés des exposés

Conception assistée de contrôleurs d'automates depuis des modèles UML
Pascal André et Yannis Le Bars

Le logiciel prend une place de plus en plus prépondérante dans les systèmes cyber-physiques, notamment grâce aux performances accrues des réseaux. Dans l’industrie du futur, le logiciel doit non seulement être de qualité en terme en fiabilité et de performance mais il doit aussi pouvoir évoluer rapidement et s’adapter aux nouveaux besoins ou à de nouvelles contraintes. L’ingénierie des modèles vise à raccourcir le cycle de développement en plaçant l’accent sur les abstractions et en automatisant partiellement la génération du code. Dans cet article, nous explorons l’assistance au passage progressif du modèle au code pour réduire le temps entre l’analyse et la production du logiciel. Le modèle couvre des aspects structurels, dynamiques et fonctionnels du système étudié. Le code visé est celui d’un système distribué sur plusieurs dispositifs. Nous préconisons une approche par transformation de modèles dans laquelle les transformations restent simples, la complexité se trouve dans le processus de transformation qui se veut adaptable et configurable. Pour mener les expérimentations, les modèles sont écrits en UML (ou SysML) et les programmes déployés sur Android et Lego EV3.


Vers une conception de systèmes synchrones réactifs sûrs
Sarah Chabane, Rabea Ameur-Boulifa et Mohamed Mezghiche

La nécessité de gérer la complexité croissante des systèmes en général, et les systèmes embarqués en particulier pousse leur conception vers une approche basée sur la réutilisation de composants existants. A cette complexité s’ajoute des exigences techniques, les systèmes doivent satisfaire des contraintes strictes de fiabilité et de correction. Dans notre travail, nous préconisons d’offrir un cadre théorique pour le développement de composants réactifs synchrones sûrs de manière compositionnelle. Dans ce papier nous offrons d’une part, un cadre de description de composants réactifs synchrones élémentaires dans un formalisme adapté pour la vérification formelle de propriétés de sûreté, et d’autre part, un cadre pour la construction des systèmes globaux à partir de composants élémentaires par une opération de composition garantissant la correction par construction.


Contrôle des SED avec urgence, évitabilité et inéluctabilité
Jean-Luc Béchennec, Didier Lime et Olivier (H.) Roux

La synthèse de contrôleurs pour les systèmes réactifs peut être faite en calculant les stratégies gagnantes dans les jeux à deux joueurs. Les automates (à jeu) temporisés sont un formalisme approprié pour modéliser les systèmes embarqués temps réel mais ne sont pas faciles à utiliser pour la synthèse de contrôleurs pour deux raisons : i) les modèles temporisés nécessitent la connaissance des temps précis du système (par exemple, si une action doit se produire à l’avenir, la date limite de cette action doit être connue) ii) Dans la pratique, la taille de l’espace d’états rend le calcul du contrôleur souvent impossible pour les systèmes complexes. Cet article présente une extension des automates à jeu non temporisés avec du temps logique. La nouvelle sémantique introduit deux nouveaux types d’actions incontrôlables : des actions non immédiates qui peuvent éventuellement être évitées par exemple par une action contrôlable effectuée en urgence, et des actions inéluctables qui finiront par se produire si rien n’est fait pour les annuler. Le problème de synthèse de contrôleur est adapté à cette nouvelle sémantique. Cet article se concentre spécifiquement sur les objectifs d’accessibilité et de sûreté et donne des algorithmes pour générer un contrôleur. L’utilité de ce nouveau modèle est illustrée par un exemple de synthèse de pilotes de périphériques.


Réification des accélérations pour la construction de Karp et Miller
Alain Finkel, Serge Haddad et Igor Khmelnitsky

L'algorithme de Karp et Miller est basé sur une exploration de l’arbre d’accessibilité d’un réseau de Pétri où on accélère les séquences de transitions à incidence positive. Les nœuds de l'arbre de Karp et Miller sont étiquetés par un ensemble d'ω-marquages représentant l'ensemble (potentiellement infini) de couverture Cover. Cet ensemble d’ω-marquages permet de décider la couverture d’un marquage ou la finitude de l’ensemble d’accessibilité. Les arcs de l’arbre de Karp et Miller sont étiquetés par des transitions mais la sémantique de celles-ci n’est pas toujours la sémantique de base ce qui rend la preuve de l’algorithme relativement compliquée. Nous introduisons ici trois nouveaux concepts : l’abstraction, l’accélération et la séquence d’exploration. En particulier, nous généralisons la définition des transitions aux ω-transitions afin de pouvoir représenter une accélération par une ω-transition. La notion d’abstraction permet de simplifier grandement la preuve de correction de l’algorithme de Karp et Miller. D’autre part, au prix d’un surcoût minime en mémoire, évalué théoriquement, nous proposons une variante « accélérée » de l’algorithme de Karp et Miller avec un gain escompté en temps d’exécution et dont la preuve de correction se déduit très simplement de notre preuve de l’algorithme de Karp et Miller.


A new analytical model for calculating elasticity in cloud computing
Assia Outamazirt, Kamel Barkaoui et Djamil Aïssani

One of the fundamental characteristics of Cloud Computing is its elasticity. It is about the ability to dynamically adapt computer resources consumption to workload while maintaining performance and quality of service. Most current industrial as well as academic solutions have limitations in terms of elasticity control, which affects the availability and performance of systems. In this paper, we propose a modeling of an elastic Cloud platform in terms of the markovian queuing model where the number of active servers depends on the current workload. A quantitative analysis of the steady state of our model allows to analyze and calculate the value of the elasticity in a precise way.


A linear time algorithm for computing off-line speed schedules minimizing energy
Bruno Gaujal, Alain Girault et Stéphan Plassart

We consider the classical problem of minimizing off-line the total energy consumption required to execute a set of n real-time jobs on a single processor with varying speed. Each real-time job is defined by its release time, size, and deadline (all integers). The goal is to find a sequence of processor speeds, chosen among a finite set of available speeds, such that no job misses its deadline and the energy consumption is minimal. Such a sequence is called an optimal speed schedule. We propose a linear time algorithm that checks the schedulability of the given set of n jobs and computes an optimal speed schedule. The time complexity of our algorithm is in O(n), to be compared with O(n log(n)) for the best known solutions. Besides the complexity gain, the main interest of our algorithm is that it is based on a completely different idea: instead of computing the critical intervals, it sweeps the set of jobs and uses a dynamic programming approach to compute an optimal speed schedule. Our linear time algorithm is still valid (with some changes) with an arbitrary power function (not necessarily convex) and arbitrary switching times.


Synthèse de contrôleurs Réseaux de Petri pour le routage dynamique des trains dans un nœud ferroviaire
Paul Cazenave, Manel Khlif-Bouassida et Armand Toguyéni

Cet article présente une méthode de prévention des collisions et des blocages pour le routage automatique des trains dans les nœuds ferroviaires. La méthode de contrôle proposée doit permettre d’optimiser le nombre de trains traversant simultanément le nœud ferroviaire. Le routage des trains est fait de manière dynamique, les trains ne suivent pas un itinéraire mais s’adaptent aux aléas du réseau. Cette approche permet d’avoir une flexibilité et une densité de trains accrue dans les nœuds ferroviaire. Mais elle doit garantir la sécurité du système et notamment l’absence de collisions entre trains dans le nœud. Pour cela, nous proposons la construction par synthèse d’un Réseau de Petri initial permettant à chaque train d’utiliser et de libérer les ressources au fur et à mesure de sa progression dans le nœud ferroviaire. Mais ce modèle initial peut entrainer un contrôle bloquant. Ainsi nous proposons une méthode de résolution des blocages potentiels permettant de garantir la vivacité du modèle final.


Gestion d’une flotte de véhicules automatisés dans un environnement portuaire
Danloup Nicolas, Trouillet Benoît, Toguyéni Armand et Bourdeaud’huy Thomas

Le transport de marchandises intègre un grand nombre de problème d’optimisation tout au long de la chaîne logistique. Cet article est dédié à la problématique de chargement/déchargement de containers dans un environnement portuaire. L’automatisation des processus est devenue une priorité pour les plus grands acteurs du secteur portuaire contraints de s’adapter à la croissance du volume de containers transportés liée à la globalisation de l’économie mondiale et aux capacités des nouvelles générations de bateaux. La concurrence entre terminaux et la nécessité de réduire les délais de chargement et déchargement des bateaux nécessitent de la part des opérateurs portuaires une augmentation de la productivité globale, une réduction des coûts d’exploitation tout en garantissant une sécurité maximale. Cet article propose la description d’algorithmes qui permettent de trouver des solutions faisable pour le problème de routage d’une flotte d’AGV, dans un temps raisonnable. La résolution exacte du problème montre très vite ses limites lors du passage à l’échelle. L’approche proposée ici est de coupler une résolution exacte avec des heuristiques. L’idée est de proposer des éléments de solution dans le but de faire chuter la complexité intrinsèque de ce type de problème. Ainsi, une solution peut être proposée avec un temps de résolution raisonnable vis à vis des contraintes imposées par les opérateurs portuaires.


Model checking paramétrique statistique du plan de vol de drone civil
Ran Bao, Christian Attiogbe, Paulin Fournier et Didier Lime

Les drones sont maintenant très répandus dans la société et sont souvent utilisés dans des situations dangereuses pour le public environnant. Il est alors nécessaire d’étudier leur fiabilité, en particulier dans le contexte de vols au-dessus d’un public. Dans cet article, nous étudions la modélisation et l’analyse de drones dans le contexte de leur plan de vol. Pour cela, nous construisons un modèle probabiliste paramétrique du drone et l’utilisons ainsi que son plan de vol pour modéliser la trajectoire du drone. Ce modèle prend en compte des paramètres comme la défaillance éventuelle du filtre ou du capteur (comme le GPS), ainsi que la force et la direction du vent. Du fait de la nature et de la complexité des modèles successifs obtenus, leur vérification avec les outils PRISM ou PARAM est impossible. Nous développons donc une nouvelle méthode d’approximation, appelée Parametric Statistical Model Checking, afin de calculer les probabilités de défaillance du drone. Cette méthode a été implémentée dans un prototype, que nous avons utilisé pour résoudre des difficultés complexes dans une étude de cas réelle.


Approche et cadre de modélisation pour l’évaluation de l’impact de perturbations sur un ordonnancement
Sara Himmiche, Pascale Marangé, Alexis Aubry et Jean-François Pétin

L’ordonnancement de la production est un problème majeur aussi bien dans le monde industriel que celui de la recherche théorique. Ce problème est généralement traité dans le but de proposer des ordonnancements optimaux. Dans le cadre d’un environnement de production dynamique, la génération classique d’ordonnancements n’est plus suffisante. La question importante qui se pose aujourd’hui est: Comment prendre en compte les contraintes de flexibilité et d’agilité qui caractérisent ces systèmes et leurs perturbations, dans le choix de l’ordonnancement à exécuter ? Cet article répond à cette question en proposant une approche générique pour évaluer la robustesse d’un ordonnancement face aux perturbations. L’approche proposée est basée sur des modèles de systèmes à événements discrets stochastiques et une méthode d’évaluation par model-checking, dans le but de définir une approche et un cadre de modélisation modulaire. Plus précisément, les automates temporisés stochastiques sont utilisés dans le but de modéliser le problème d’ordonnancement sous perturbations et le model- checking statistique est utilisé pour évaluer ces modèles et ainsi permettre le calcul d’un indicateur de robustesse qui sera transmis au décideur.


ETVO: librairie C++ pour la description des Graphes d’Evénements Temporisés valués
B. Cottenceau, L. Hardouin et J. Trunk

La librairie ETVO est destinée aux calculs sur des expressions rationnelles constituées sur un ensemble d’opérateurs {γn, δt, μm, βb, ∆T} utilisées pour d’écrire le comportement dynamique de certains systèmes à événements discrets temporisés. Sont concernés par cette approche : les Graphes d’Evénements Temporisés (GET) avec arcs valués et les GET avec temps de séjour cycliques. Pour ces deux classes de systèmes, la librairie ETVO permet le calcul de transfert et la synthèse de contrôleurs.


The tool TWINA – construction d'espaces d'états abstrait pour l'intersection de Time Petri nets
Éric Lubat

Dans ce travail, nous présentons un nouvel outil, TWINA, qui permet de calculer une abstraction par graphes de classes pour « l'intersection » de deux TPN ; c'est-à-dire une abstraction permettant d'analyser de manière exacte les séquences de tirs, ou traces, qui sont communes à deux réseaux. Dans notre contexte, on ne retient que les étiquettes (les labels) des transitions. Ainsi, une trace est commune à deux TPN lorsqu'il est possible de tirer une séquence de transitions ayant les bons labels, dans le bon ordre et au même dates, dans les deux réseaux. En tant que tel, TWINA permet de raisonner sur l'intersection du langage de plusieurs TPN. Plus généralement, TWINA permet l'analyse du « produit synchrone » de TPN, un modèle appelé Product Time Petri Net. Intuitivement, il s'agit d'une extension des TPN dans laquelle on impose que toutes les transitions de certains ensembles donnés soient tirées en même temps. Cette opération est utile dans la pratique, par exemple pour des applications de vérification des modèles -afin de pouvoir vérifier des propriétés temporisées par l'utilisation d'observateurs, mais sans risquer d'interférences avec le système à étudier- ou bien encore, dans le domaine du diagnostic, afin de définir une construction équivalente à celle de la twin plant dans le cas des TPN.


Une algèbre des automates d’acceptation propositionnelle déterministes comme théorie d’interface pour la conception de systèmes cyberphysiques
Aurélien Lamercerie

Les systèmes cyberphysiques (CPS) sont des logiciels fonctionnant en interaction étroite avec des périphériques physiques. Leur spécification est une tâche complexe et source d’erreurs. Leur conception résulte de l’assemblage de composants, souvent conçus par des équipes multidisciplinaires indépendantes. Chaque équipe doit non seulement spécifier le comportement attendu du composant en cours de conception, mais également énoncer les hypothèses sous lesquelles le composant doit fonctionner. Au moment de l’intégration, ces hypothèses doivent être vérifiées par rapport au comportement du système, pris dans sa globalité. Le raisonnement par contrats est une méthode intégrée à plusieurs langages de programmation, inspirés de la logique de Hoare et d’extensions de celles-ci. Détecter les erreurs de spécification aussi tôt que possible permet d’économiser beaucoup de temps, d’efforts et d’argent. Formaliser les besoins, les analyser par des méthodes automatiques ou assistées par ordinateur, ou les vérifier à l’exécution, sont essentielles pour détecter des exigences incohérentes, redondantes ou incomplètes. Dans le contexte de la conception de CPS, les théories d’interface permettent de décrire en une seule spécification à la fois le comportement attendu d’un composant et les environnements possibles dans lesquels il peut être exécuté. Les exemples typiques de théories d’interface sont les automates d’interfaces et les interfaces modales. Ces formalismes basés sur la théorie des automates sont capables d’exprimer à la fois la variabilité des conceptions possibles et les incertitudes concernant les environnements possibles d’un composant. Néanmoins, ces théories ne traitent que de la relation entre les entrées et les sorties de composants réactifs. Dans de nombreux cas, il serait souhaitable de relier ces comportements d’entrée/sortie à l’état du composant. Notre contribution, les automates d’acceptation propositionnelle déterministe (Determinitic Propositional Acceptance Automata, DPAA), est une réponse à cette question. Ces automates permettent de spécifier des comportements de temps discret, obligatoire ou interdit. La caractéristique principale de ce formalisme est qu’il permet d’exprimer le comportement attendu lorsque le système est dans un état particulier. Les DPAA combinent des propriétés d’état, exprimées sous forme de formules propositionnelles, et des propriétés temporelles discrètes, exprimées sous forme d’événements obligatoires ou interdits. Ils étendent les systèmes de transition modaux en prenant comme modèles les structures de Kripke plutôt que des systèmes de transition étiquetés.


Algorithm for controlling the transient behavior of controlled generalized batches Petri nets
Ruotian Liu, Rabah Ammour, Leonardo Brenner et Isabel Demongodin

Discrete Petri nets (PNs) are widely used for modeling, analysis and control discrete event systems but suffer from the state explosion problem. To overcome this issue, several works have been developed on a relaxation technique so-called fluidization of Petri nets models, thus extending the discrete formalism to continuous PN. The combination of both, discrete and continuous PNs, has allowed the definition of hybrid Petri nets. By introducing in hybrid PNs a new kind of nodes, called batch nodes, generalized batches Petri net (GBPN) enriches the class of hybrid models. Based on the concept of batches as marking, i.e., a group of entities moving through a zone at a certain speed, GBPN is appropriate for describing the behavior of high throughput production lines (control design and performance of high-speed systems), transmission delay on a communication media with bus topology, interlocking system design for ERTMS/ETCS, multimodal systems or transportation networks. In order to drive the evolution of the model, controlled GBPN (cGBPN) considers as control inputs the firing flow of continuous and batch transitions and the transfer speed of batch places. One important behavior which characterizes dynamic systems is the steady state. In a cGBPN without discrete nodes, a steady state is characterized by the couple (ms, φs) where ms is a constant marking and φs is constant vector of instantaneous firing flows. Our objective is to control the transient trajectory of a cGBPN. By assuming that there are no discrete nodes and all transitions are controllable, the problem is how to reach a target steady state (ms, φs) from a given initial marking m0, by controlling only the instantaneous firing flow of transitions. Much efforts have been devoted to the control design for trajectory tracking with continuous Petri nets while few works have been conducted on hybrid PNs or cGBPNs.


Analyse d’atteignabilité des systèmes (max,+)-linéaires à l’aide des polyèdres tropicaux
Guilherme E. Winck, Mehdi Lhommeau et Laurent Hardouin

Les Systèmes à Evénements Discrets (SED) peuvent être définis comme des systèmes dans lesquels les variables d’état changent sous l’occurrence d’évènements au fil du temps. Les SED mettant en jeu des phénomènes de synchronisation peuvent être modélisés par des équations linéaires dans les algèbres de type (max,+). Dans ce papier, on s’intéresse au problème de l’atteignabilité des SED décrits dans l’algèbre (max,+). L’objectif est de déterminer l’ensemble atteignable des SED décrits dans l’algèbre (max,+), c’est-à-dire l’obtention de toutes les trajectoires d’état générées à partir d’un domaine d’état initial. L’approche proposée repose sur la théorie des polyèdres tropicaux.


Integrated Modeling Proposal of Supervisory Control Theory and Model-Based System Engineering
Xiaoshan Lu, Laurent Piétrac et Eric Niel

The Supervisory Control Theory (SCT), firstly introduced by Ramadge and Wonham in 1987, is one of the most important paradigms of formal modeling, control synthesis and verification for Discrete Event System (DES). The large number of scientific contributions shows that SCT catches extensive academic interest and this theory has been proved to be applicable in various industrial domains such as manufacturing systems, embedded systems or energy systems, etc. With SCT, the requirements which are checked afterward in traditional engineering are used as input for generation of the design of the controller that is correct by construction. By the scientific achievements within the past several decades, the framework of SCT forms a systematically formal paradigm to synthesize controllers for DESs and a series of concepts and methods are proposed. However, despite the academic achievements of SCT, there are still gaps between the theoretical development and applications of SCT in engineering practice. Firstly, there is a lack of interpretation between informal requirements and formal specifications in typical development process. Systems’ requirements are usually written in an informal narrative since it generally means a greater understanding among the various stakeholders. On the other hand, formal models such as automaton have unambiguous semantic, which means a model cannot be understood in different ways. It is still difficult to link the formalization and informal narrative requirements. Secondly, as the formal model can only represent the behavior of system to be studied, it is difficult to describe the structure aspect, which includes both physic and logic. The gap between plants and physic components leads to the problem: supervisor/controller may also be structured. Unfortunately, there is no model can be used to explicitly describe the details of the structure. The existing contributions focus on how to transform the supervisor to the software and hardware aspect of concrete controller is neglected. In fact, it leads to problems of controller implementation. In fact, these two situations are due to ambiguity for hardware and software and lack of the implementation models. The existing supervisory control architecture and implementation methods are not able to specify the link between the models of supervisor/controller and models of concrete controller, which is unacceptable in the engineering the consistency between plants and physic components is unclear. Besides, the context. Finally, the SCT does not provide the global modeling process from analyzing and decomposing the informal requirements to sub-systems to transform models to implementation. The Model-Based System Engineering (MBSE) provides the possibility to deal with the limitations of SCT. MBSE is the actual state-of-the-art global design process in engineering practice. A variety of modeling languages are proposed by OMG for realizing the MBSE methods. Especially, SysML is one of the most important modeling languages, which provides nine kinds of diagrams to be used to describe different aspect of the system. The main objective of the work is to propose an integrated modeling framework for controller development by combining Supervisory Control Theory with Model-Based System Engineering to bridge the gaps formal approach and engineering process. In the proposed framework, different SysML diagrams are used to as complementary models, which present the indispensible views of the system to be studied in the global modeling process. The proposed framework focuses on the improvement of the traceability, consistency and reusability, compared with the conventional SCT-based modeling process.


A Tool for the Coverability Problems in Petri Nets
Alain Finkel, Serge Haddad et Igor Khmelnitsky

Petri nets are an infinite-state model for specification and verification of concurrent systems. An important generic problem of this model is coverability, which asks p the following question: Given a Petri net N and two markings m0, mt ∈ Np, does there exist a firing sequence σ such that m0 σ m’ ≥ mt. Another related problem, is the coverability set problem which asks: Given → a Petri net N and an initial marking m0, produce a finite set Clover(N, m0) of markings such that a marking m is coverable if there exists an ω-marking m’ ∈ Clover(N, m0) such that m’ ≥ m. The computational complexity of these problems is very high: The coverabilty problem is EXPSPACE-complete while the size of the coverabilty set may be non primitive recursive. The tool CovMin was designed to efficiently solve these problems.


Pronostic des événements de défaillances basé sur les réseaux de Petri temporels labellisés
Redouane Kanazy, Samir Chafik, Eric Niel et Laurent Piétrac

Les applications de supervisions mises à la disposition des développeurs de systèmes de contrôles qui opèrent dans les domaines de la production manufacturière, la robotique, la logistique, la circulation des véhicules, les réseaux de communication ou l’informatique, permettent de signaler la détection d’un disfonctionnement ou d’un arrêt accidentel du système et de localiser son origine. La communauté des systèmes à événements discrets (SED) a développé des méthodes de diagnostic qui s’intéressent à l’enchaînement logique, dynamique ou temporel des événements de défaillance qui sont source de ce disfonctionnement. Cependant, la criticité de certains systèmes et leur complexité nécessitent une méthode de pronostic de ces événements de défaillance, pour signaler leurs occurrences à l’avance afin éviter tout dommage causé par une panne. La difficulté serait alors de savoir comment signaler l’occurrence future d’un événement de défaillance. Quel outil de modélisation est adapté pour ce type de système ? Sachant que plus la complexité du système est élevée, plus son espace d’états est important. La question que l’on se pose donc est comment surmonter le problème d’explosion combinatoire ? Quelles sont les limites du pronostic?


Approche distribuée pour la reconfiguration de la commande des systèmes manufacturiers
Imane Tahiri, Alexandre Philippot, Véronique Carre-Menetrier et Abdelouahed Tajer

Dans cet article, nous proposons une approche pour la reconfiguration de la commande des systèmes à événements discrets. La contribution est basée sur une synthèse de contrôle sûr de fonctionnement en exploitant une architecture distribuée incluant des événements temporisés. Lorsqu’un défaut est détecté sur un capteur, le contrôleur du comportement normal est reconfiguré en un contrôleur de comportement fautif où des informations temporisées compensent les informations perdues par le capteur défectueux. L’approche est appliquée sur un système simple de transfert de caisses.


Modèles à base d’opérateurs pour les systèmes (max,+) cycliques
B. Cottenceau, L. Hardouin et J. Trunk

Certaines classes de Systèmes à Evénements Discrets (SED) peuvent être étudiées via des modèles sur des dioïdes, notamment en décrivant leur dynamique au moyen d’opérateurs. Le décalage temporel et le décalage dans la numérotation des événements sont dans ce cas assimilés à des opérateurs élémentaires. Depuis les années 80, cette approche a permis l’étude des Graphes d’Evénements Temporisés (GET) au travers de modèles entrée-sortie. La structure algébrique considérée est alors un ensemble de séries formelles, noté , dont les variables γ et δ sont assimilables aux opérateurs mentionnés ci-avant. Il a été montré que l’on peut étendre cette approche en considérant de nouveaux opérateurs additifs et ainsi contribuer à l’étude de systèmes mettant en jeu des phénomènes comme la duplication d’événements (opérateur μm), le regroupement (opérateur βb), ou encore des synchronisations temporelles spécifiques (opérateur ∆T). A la différence des GET ordinaires, les systèmes impliquant de tels phénomènes ne sont alors plus stationnaires. Ils conservent néanmoins une propriété de cyclicité, dans le domaine temporel ou événementiel, qui rend leur étude plus complexe, mais possible. Les techniques de calcul pour les systèmes cycliques sont d’ailleurs comparables à celles utilisées pour les séries périodiques de MinMax[[gamma,delta]] Ce papier vise à introduire la librairie logicielle ETVO ((Event|Time) Variant Operators) qui a été développée pour les calculs sur les systèmes cycliques. Des rappels de modélisation sont tout d’abord donnés avant de montrer comment traiter quelques exemples simples à l’aide de l’outil ETVO. Cet outil de calcul permet l’analyse de performance et la synthèse de contrôle pour les GET ordinaires, les GET valués et les GET avec des temps de séjour cycliques.


Commande sous contraintes temporelles des réseaux de graphes d’événements temporisés en conflit
Sofiane Aberkane, Redouane Kara et Said Amari

Dans ce papier, nous abordons le problème de modélisation et de commande des systèmes à événements discrets avec des ressources partagées représentés par une classe particulière des réseaux de Petri temporisés. Précisément, nous considérons des Réseaux de Graphes d’Evénements Temporisés en Conflit (RGETC) soumis à des contraintes temporelles strictes. Premièrement, une formalisation algébrique en termes de systèmes à commutation Max-Plus est proposée pour décrire le comportement dynamique des RGETCs. Deuxièmement, des lois de commande en boucle fermée sont calculées pour garantir le respect de ces contraintes de temps imposées à certaines places du réseau. Des conditions suffisantes pour l’existence de telles lois de commande ont été fournies. Finalement, nous appliquons les résultats théoriques développés précédemment pour contrôler un système ferroviaire de croisement de train à temps critique.