Search

National audience

6 pages; International audience; Ce papier présente une classe d'automates hybrides à haut niveau d'expressivité pour faciliter la modélisation modulaire des Systèmes Dynamiques Hybrides (SDH) : les automates hybrides à entrées/sorties et synchronisations typées. Elle combine le concept de modularité issue des automates à entrées/sorties avec plusieurs mécanismes de synchronisation par étiquette de transition. Afin d'exploiter un tel modèle avec les outils existants nous proposons (i) un opérateur de composition pour fournir un automate "mis à plat", et (ii) un algorithme de traduction des mécanismes de synchronisations typées en classiques synchronisations par rendez-vous. L'intérêt de notre classe d'automates hybrides pour la modélisation modulaire est mis en évidence sur un exemple de SDH qui nous permet également d'illustrer l'opérateur de composition et l'algorithme de traduction des mécanismes de synchronisations typées.

International audience; This paper focuses on bus communication networks where every terminal is modeled as a multi-states component with a propagating failure state. An analytic expression of the reliability of the transmission between two terminals is first computed. From that, it is shown that partitioning the bus may lead to increase, decrease or let unchanged this reliability, according to the positions of the considered terminals in the different partitions. This analysis is aiming at providing an efficient help for the designers of communication networks of critical systems.

6 Pages; National audience; Ce papier présente une méthode originale pour obtenir une expression analytique de la fiabilité d'une transmission de données entre deux terminaux d'un système en réseau dans lequel les composants peuvent comporter plusieurs modes de défaillance et où certaines de ces défaillances peuvent se propager à des composants adjacents. Cette contribution est illustrée sur une architecture typique des systèmes critiques ; la comparaison à une approche classique, dans laquelle un seul mode de défaillance est retenu et la propagation des défaillances est ignorée, permet de montrer les bénéfices que procure cette proposition.

National audience; Ce papier présente une méthode qui facilite la conception de l'architecture opérationnelle d'un système de commande en proposant, à partir de la connaissance des caractéristiques des fonctions que doit assurer ce système et des contrôleurs choisis pour réaliser ces fonctions, une solution d'affectation des fonctions qui satisfait des contraintes de capacités et de répartition tout en minimisant le nombre de contrôleurs. Cette méthode repose sur la vérification d'une propriété d'atteignabilité sur un réseau d'automates communicants. L'intérêt de cette proposition est illustré par le traitement d'un cas non trivial issu de la réalité industrielle.

International audience; The use of Ethernet at the field level seems to be the next step after traditional fieldbusses. Even if it was not used to be competitive compared to solutions designed for industrial purpose, Ethernet performances have increased faster. On the other hand, some special features like net- work availability solutions have not improved so much rapidly. Then faster Ethernet based industrial protocols had to specify accurate solutions. The objective of this paper is to validate the medium redundancy management part of the Ethernet PowerLink High Availability extension. For this, aimed application requirements are stated and the protocol with its extension are detailed. In the context of Alstom Power critical appli- cations, the correctness of the solution of redundancymust be proven. Therefore, a model-checking approach is used from a generic modelling in timed finite state automata.

The use of a plant model for formal verification of industrial controllers makes the formal verification tasks more realistic, because any industrial system is always composed by a controller and a plant. Therefore, if the plant model is not used, there is a part of the system that is not considered. However, if there are some cases where the use of a plant model becomes the formal verification results more realistic and robust there are other cases where it nor always happens. In this paper there are indicated which are the circumstances where it is useful to use, or not, a plant model on formal verification tasks, using model-checking techniques.

International audience; L'idée d'avoir un média universel comme bus de terrain est séduisante. Ainsi, le développement de composants d'automatisation communicant sur un réseau Ethernet commuté utilisant des protocoles de communication standards et ouverts est d'actualité. Cependant, ce type de réseau introduit des mécanismes de partage de ressources et d'asynchronisme entre processus parallèles. Pour les architectures devant assurer la commande de systèmes à événements discrets, la conjonction de ces mécanismes rend difficile l'évaluation du délai de réactivité, retard entre l'occurrence d'un événement et celle de sa conséquence sur le processus. Nous proposons dans cet article une méthode basée sur la simulation d'un modèle dynamique en réseau de Petri hiérarchique coloré temporisé qui prend en compte les mécanismes d'asynchronisme et de partage de ressources. Deux cas tests permettent de mettre en évidence l'intérêt de la modélisation proposée.

International audience; Programmable Logic Controllers ensure the control of many reactive systems. These controllers are most of the time programmed with the languages defined in the IEC 61131-3 standard. Our goal is the verification of safety properties of programs written in one of these languages: the Ladder Diagram. The main approaches in this field are based on Model-Checking. We propose in this article a Theorem-Proving method by defining a formal framework to express and handle the Ladder Diagram programs with a specific algebra. Firstly, we translate the specific statements of the language into this algebra and we give some general theorems. Then, we present on an example an analysis leading to the verification of safety properties.

Article dans revue scientifique avec comité de lecture.; The general objective of the project is to build a process-centred environment kernel, providing assistance and active guidance to its users. Thanks to an hybrid approach of process modelling, both task-oriented at a coarse grain level, and decision-oriented at a fine grain level, it can be customized to support a broad range of collective design activities. The concept of issue is central to the modelling approach, both on the design side, for decision-oriented modelling of creative activities, and on the cooperation side, for modelling collective conflict resolution tasks. The paper reports some initial experiences with the current prototype (CPCE), customized for supporting collective code inspections. This experiment demonstrates the concrete feasibility of the approach.

International audience

International audience

Not available, Les travaux exposés dans ce mémoire portent sur la conception de l'architecture de conduite des systèmes automatisés de production. Ils ont été développés au sein du laboratoire universitaire de recherche en production automatisée (lurpa ea 1385). Il s'agit de travaux prospectifs dont l'objectif est de construire un cadre méthodologique formel de conception et d'évaluation d'architectures. La première partie est consacrée à l'expose du cadre méthodologique retenu et comporte quatre chapitres dans lesquels sont successivement abordés: 1) la problématique générale de la conception d'architectures de conduite, ainsi qu'une revue des travaux scientifiques dans le domaine; 2) la présentation générale de la méthode proposée avec le point de vue des activités de conception, d'évaluation et de choix d'architecture; 3) la présentation détaillée de la construction d'architecture avec cette fois le point de vue des différents modèles produits; 4) la présentation détaillée d'évaluation et de choix de l'architecture retenue avec encore une fois le point de vue des modèles d'évaluation. La seconde partie du mémoire est destinée à préciser et à valider par l'exemple la méthode proposée. Pour ce faire, nous l'avons appliquée à la conception de l'architecture de conduite d'un poste de lancement d'un transfert libre. Le plan de cette étude suit de manière ordonnée la démarche que nous avons présentée dans la première partie

International audience

National audience; Natural mating of a doe with a ram produced a female hybrid carrying 57 chromosomes, including three metacentric autosomes. This animal backcrossed to a Solognot ram delivered a stillborn and a living male offspring. The karyotype of this last animal consisted of 54 chromosomes.; L’accouplement naturel d’une chèvre avec un bélier a produit une femelle hybride fertile dont le caryotype composé de 57 chromosomes comprend trois autosomes métacentriques. Celle-ci, saillie par un bélier Solognot, a mis bas deux mâles, l’un mort-né et l’autre vivant. Le caryotype de ce dernier était composé de 54 chromosomes.

National audience

International audience

National audience

National audience; Suite a des etudes comprenant, d'une part des donnees du centre d'economie rurale et de gestion d'Ille-et-Vilaine (CERGIV), d'autre part une enquete realisee aupres d'eleveurs, les auteurs confirment que les frais veterinaires, en elevage bovin laitier, representant 4 a 5 pour cent des charges variables et montrent que les trois postes les plus importants sont les mammites et soins de la mamelle (22,8 pour cent), l'ensemble infecondite-metrites (12,6 pour cent) et la prophylaxie reglementaire (10,9 pour cent). Les actions preventives interviennent au total pour 22 pour cent du cout veterinaire. Les frais sanitaires varient en meme temps qu'un certain nombre de parametres techniques et economiques, l'essentiel etant qu'ils s'accroissent en moyenne en meme temps que les autres charges variables. C'est au travers de l'augmentation generalisee de ces dernieres que doit etre d'abord compris l'accroissement des depenses veterinaires avec l'intensification et le niveau de production laitiere par vache.

National audience

9 pages; International audience; The performances of automation systems are strongly linked to the performances of their control architecture. These architectures are the merger of a hardware structure – industrial computers and logic controllers connected to networks and fieldbuses – and of software components – implantation control functions. To manage these performances, the control engineer must evaluate them at each stage of the life cycle: from the project requirements to the setup stage, including the detailed design. In this paper, we present a method which evaluates timed performances of networked automation system and which guides the engineer throughout the control architecture development. A modular design has been retained to model the dynamic behaviour of the control architecture using Timed Coloured Petri Nets. To begin we present the design of generic modular models and we explain how these modules are instantiated and assembled to build the dynamic model of a whole control architecture. Next we present some enrichments of the assembled model in order to simulate the behaviour of the control architecture. These complements are some event generators – to excite the models – and some event observers – to detect, to date and to log the relevant events. Then we present the simulation results of four different timed performances on the same architecture. These results take the form of histograms of 10,000 simulated delays for each evaluated performance. Finally, the method suggested for the model construction is validated. by confrontation between the results of model simulation and the measurement of the real control architecture.