Search

Global Navigation Satellite Systems (GNSS) such as GPS, already used in aeronautics for safety-related applications, can play a major role in railway safety by allowing a train to locate itself safely. However, in order to implement this positioning solution in any embedded system, its performances must be evaluated according to railway standards. The evaluation of GNSS performances is not based on the same attributes class than RAMS evaluation. Face to these diffculties, we propose to express the integrity attribute, performance of satellite-based localisation. This attribute comes from aeronautical standards and for a hybridised GNSS with inertial system. To achieve this objective, the integrity attribute must be extended to this kind of system and algorithms initially devoted to GNSS integrity monitoring only must be adapted. Thereafter, the formalisation of this integrity attribute permits us to analyse the safety quantitatively through the probabilities of integrity risk and wrong-side failure. In this paper, after an introductory discussion about the use of localisation systems in railway safety context together with integrity issues, a particular integrity monitoring is proposed and described. The detection events of this algorithm permit us to conclude about safety level of satellite-based localisation system.

ANT 2018, The 9th International Conference on Ambient Systems, Networks and Technologies, Porto, PORTUGAL, 08-/05/2018 - 11/05/2018; Protocol design is usually based on the functional models developed according to the needs of the system. In Intelligent Transport Systems (ITS), the features studied regarding Vehicular Ad hoc Networks (VANET) include self-organizing, routing, reliability, quality of service, and security. Simulation studies on ITS-dedicated routing protocols usually focus on their performance in specific scenarios. However, the evolution of transportation systems towards autonomous vehicles requires robust protocols with proven or at least guaranteed properties. Though formal approaches provide powerful tools for system design, they cannot be used for every types of ITS components. Our goal is to develop new tools combining formal tools such as Event-B with DEVS-based (Discrete Event System Specification) virtual laboratories in order to design the models of ITS components which simulation would allow proving and verifying their properties in large-scale scenarios. This paper presents the models of the different components of a VANET realized with the Virtual Laboratory Environment (VLE). We point out the component models fitting to formal modeling, and proceed to the validation of all designed models through a simulation scenario based on real-world road traffic data.

Processing specifications is an issue of crucial importance when developing critical complex systems. In particular, establishing rigorous specifications broadly impacts the subsequent engineering phases. This paper discusses a refinement technique for processing informal specifications expressed in a literal shape, with the aim to generate formal specifications appropriate to automatic processing. The developed technique carries out an iterative process which relies on a set of basic refinement patterns that we have established, and ends up with a formalization step which actually generates logical CTL* formulas. Furthermore, the method implements traceability facilities, which allow for a tidy backtracking of the whole process. The concepts introduced to set up the various mechanisms are discussed and a case study featuring an embedded railway control system is used to illustrate our technique.

The work in the article presents the development of an application guide based on feedback and comments stemming from various railway actors on their practices of SIL allocation to railway safety-related functions. The initial generic methodology for SIL allocation has been updated to be applied to railway rolling stock safety-related functions in order to solve the SIL concept application issues. Various actors dealing with railway SIL allocation problems are the intended target of the methodology; its principles will be summarized in this article with a focus on modifications and precisions made in order to establish a practical guide for railway safety authorities. The methodology is based on the flowchart formalism used in CSM (common safety method) European regulation. It starts with the use of quantitative safety requirements, particularly tolerable hazard rates (THR). THR apportioning rules are applied. On the one hand, the rules are related to classical logical combinations of safety-related functions preventing hazard occurrence. On the other hand, to take into account technical conditions (last safety weak link, functional dependencies, technological complexity, etc.), specific rules implicitly used in existing practices are defined for readjusting some THR values. SIL allocation process based on apportioned and validated THR values is finally illustrated through the example of 'emergency brake' subsystems. Some specific SIL allocation rules are also defined and illustrated.

SCVT 2017 - 24th IEEE Symposium on Communications and Vehicular Technology (IEEE SCVT), Louvain, BELGIQUE, 14-/11/2017 - 14/11/2017; The Optimized Link State Routing (OLSR) protocol, early designed for Mobile Ad hoc Networks (MANET), has been customized and evaluated for various Vehicular Ad hoc Network (VANET) scenarios. Most of the related work focus on changing OLSR parameters in order to adapt it to the high dynamicity of VANET due to high velocity of its nodes. However, they keep using OLSR with its native clustering scheme, the Multipoint Relaying (MPR). Recently, the chain-branch-leaf (CBL) clustering scheme has been proposed for road traffic configuration. This work presents a comparative analysis of CBL with MPR clustering in OLSR. The results show that CBL reduces significantly the routing traffic overhead in OLSR by reducing the number of relays, without degrading the performance for the application traffic.

Cet article s’intéresse à la diagnosticabilité des systèmes à événements discrets temporisés. Le formalisme de modélisation utilisé est le réseau de Petri T-temporel et labellisé (RdP-LT). C’est une extension des RdP temporels pour laquelle à chaque transition est associé un événement qui peut être observable ou non. Nous proposons une approche pour vérifier la diagnosticabilité et nous fournissons une solution pour calculer le délai minimum delta pour garantir cette diagnosticabilité. L’analyse de cette diagnosticabilité est effectuée par un algorithme à la volée, basé sur une structure de données que nous nommerons graphe-ECEE. Cette structure contient les informations sur l’état du RdP-LT. Les algorithmes à la volée permettent souvent d’obtenir un résultat sans avoir nécessairement à explorer tout l’espace d’états. C’est un avantage important par rapport aux approches classiques d’énumération systématique de tous les états.

Представлений системний аспект поняття «здоров'я». Наводяться загальне (родове) визначення і дефініція аспекту понять: «здоров'я індивіда», «здоров'я сім'ї» і «здоров'я населення». Останні дозволяють позначити їх індивідуальні, унікальні особливості. Конструктивність визначень створила можливість виходу на вимірювання параметрів станів об'єктів. Представлені наступні інтегрально-композиційні показники: життєвий ресурс популяції, якість його використання, напруженість способу життя, генетична життєстійкість популяції, потенціал і швидкість адаптації її в середовищі проживання, генетичні ризики виживання покоління. Вони названі прямими «власними» показниками здоров'я населення. Одночасно були отримані вимірювання якості середовища проживання населення, потенціалу середовища в стабілізації стійкого функціонування людей в ній, страхові ризики проживання в регіоні., The system aspect of the concept of "health" is presented. The general (generic) definition and definition of aspect concepts are resulted: "health of the individual", "family health" and "health of the population". The latter allow us to identify their individual, unique features. The constructiveness of the definitions has made it possible to enter the measurement of object state parameters. The following integral-composite indices are presented: the vital resource of the population, the quality of its use, the intensity of the way of life, the genetic viability of the population, the potential and speed of its adaptation in the environment of living, the genetic risks of survival of the generation. They are called direct "own" indicators of public health. At the same time, measurements of the quality of the habitat population, the potential of the environment in stabilizing the sustainable functioning of people in it, insurance risks of living in the region., L'aspect système du concept de «santé» est présenté. La définition générale (générique) et la définition des concepts d'aspect sont obtenues: «santé de l'individu», «santé de la famille» et «santé de la population». Ces derniers nous permettent d'identifier leurs caractéristiques individuelles et uniques. La construction des définitions a permis d'entrer la mesure des paramètres d'état de l'objet. Les indices intégraux suivants sont présentés: la ressource vitale de la population, la qualité de son utilisation, l'intensité du mode de vie, la viabilité génétique de la population, le potentiel et la rapidité de son adaptation à l'environnement, les risques génétiques de survie de la génération. Ils sont appelés «propres» indicateurs directs de la santé publique. En même temps, des mesures de la qualité de l'habitatla population, le potentiel de l'environnement à stabiliser le fonctionnement durable des personnes qui y vivent, les risques d'assurance de la vie dans la région., Представлен системный аспект понятия «здоровье». Приводятся общее (родовое) определение и дефиниция аспектных понятий: «здоровье индивида», «здоровье семьи» и «здоровье населения». Последние позволяют обозначить их индивидуальные, уникальные особенности. Конструктивность определений создала возможность выхода на измерение параметров состояний объектов. Представлены следующие интегрально-композиционные показатели: жизненный ресурс популяции, качество его использования, напряженность образа жизни, генетическая жизнестойкость популяции, потенциал и скорость адаптации ее в среде проживания, генетические риски выживания поколения. Они названы прямыми «собственными» показателями здоровья населения. Одновременно были получены измерения качества среды обитания населения, потенциала среды в стабилизации устойчивого функционирования людей в ней, страховые риски проживания в регионе.

nteroperability of railway systems is a major concern in the European Union. Therefore, ERTMS (European Railway Train Management System) has been defined. Nevertheless, ERTMS has to be paired with national track rules. The Perfect project studies the implementation of ERTMS on the French territory. We use an ERTMS 3D Simulator framework which is able to simulate trains, track and communication between the trains and the RBC. The simulator records all events that occur in a sequence of states called trace. Each event is timestamped, so the sequence of events can be temporally analysed. We propose a methodology to analyse the results of a scenario performed on this platform, using temporal properties. One of the strengths of this method is the computation of statistical information on the trace during its analysis, according to a dedicated pattern of property. An automatic analysis of a trace can be used in several domains. In safety, verification of critical temporal property makes sense in ensuring that a program is compliant with its specification. An analysis of an accident or near accident using temporal properties can provide a safety problem detection and a first level diagnosis. It can also be a interesting tool to evaluate the efficiency of an operator according to several criteria such as tiredness, expertise, repetitiveness of an event., L'interopérabilité d'un système ferroviaire est un problème majeur dans l'Union européenne. C'est pourquoi ERTMS (European Railway Train Management System) a été défini. Cependant ERTMS doit être associé aux règles nationales propres aux voies. Le projet Perfect étudie l'implémentation d'ERTMS sur le territoire Français. Nous utilisons un simulateur ERTMS 3D capable de simuler des trains, des voies, et des communications entre les trains et le RBC. Le simulateur enregistre chaque éÎnement ayant lieu dans une séquence d'états appelée trace. Comme chaque éÎnement est daté, la séquence d'éÎnement peut être analysée temporellement. Nous proposons une méthodologie pour analyser les résultats d'un scénario joué sur cette plate-forme, en utilisant des propriétés temporelles. Une des forces de cette méthode est le calcul d'information statistique sur la trace pendant son analyse suivant un patron de propriété donné. En terme de sûreté de fonctionnement, la Îrification de propriétés temporelles permet d'assurer que le programme correspond à sa spécification. Une analyse de scénario accidentogène utilisant des propriétés temporelle permettra de détecter des problèmes de sûreté et servir de premier niveau de diagnostique. Cela pourra être également un outil intéressant pour évaluer l'efficacité d'un opérateur suivant plusieurs critères tels que la fatigue, l'expertise, la répétitivité d'un éÎnement.

International Conference on Knowledge Engineering and Ontological Engineering, Londres, ROYAUME-UNI, 18-/01/2016 - 19/01/2016; Ontologies offer a means for representing and sharing information in many domains, particularly in complex domains. For example, it can be used for representing and sharing information of System Requirement Specification (SRS) of complex systems like the SRS of ERTMS/ETCS written in natural language. Since this system is a real-time and critical system, generic ontologies, such as OWL and generic ERTMS ontologies provide minimal support for modeling temporal information omnipresent in these SRS documents. To support the modeling of temporal information, one of the challenges is to enable representation of dynamic features evolving in time within a generic ontology with a minimal redesign of it. The separation of temporal information from other information can help to predict system runtime operation and to properly design and implement them. In addition, it is helpful to provide a reasoning and querying techniques to reason and query temporal information represented in the ontology in order to detect potential temporal inconsistencies. Indeed, a user operation, such as adding a new constraint on existing planning constraints can cause temporal inconsistencies, which can lead to system failures. To address this challenge, we propose a lightweight 3-layer temporal Quality of Service (QoS) ontology for representing, reasoning and querying over temporal and non-temporal information in a complex domain ontology. Representing QoS entities in separated layers can clarify the distinction between the non QoS entities and the QoS entities in an ontology. The upper generic layer of the proposed ontology provides an intuitive knowledge of domain components, specially ERTMS/ETCS components. The separation of the intermediate QoS layer from the lower QoS layer allows us to focus on specific QoS Characteristics, such as temporal or integrity characteristics. In this paper, we focus on temporal information that can be used to predict system runtime operation. To evaluate our approach, an example of the proposed domain ontology for handover operation, as well as a reasoning rule over temporal relations in this domain-specific ontology, are given.

Verification is decisive for embedded software. The goal of this work is to verify temporal properties on industrial applications, with the help of formal dynamic analysis. The approach presented in this paper is composed of three steps: formalization of temporal properties using an adequate language, generation of execution traces from a given property and verification of this property on execution traces. This paper focuses on the verification step. Use of anew kind of Büchi automaton has been proposed to provide an efficient verification taking into account the industrial needs and constraints. A prototype has been developed and used to carry out experiments on different anonymous real industrial applications.; L'activité de Îrification est décisive pour les logiciels embarqués. le but de ce travail est de Îrifier des propriétés temporelles sur des applications industrielles, en utilisant l'analyse dynamique formelle. L'approche présentée dans ce papier est composée de trois étapes: la formalisation des propriétés temporelles en utilisant un langage adéquate, la génération de traces d'exécution à partir d'une propriété temporelle donnée et la Îrification de cette propriété sur les traces d'exécution. Ce papier se focalise sur la phase de Îrification. L'utilisation d'un nouveau type d'automate de Büchi a été proposée pour fournir une méthode de Îrification eficace, en prenant en compte les besoins et contraintes industrielles. Un prototype a été développé et utilisé pour mener des expérimentations sur différents cas réels anonymisés d'application industrielles.

Vehicular ad hoc networking is an emerging paradigm which is gaining much interest with the development of new topics such as the connected vehicle, the autonomous vehicle, and also new high-speed mobile communication technologies such as 802.11p and LTE-D. This paper presents a brief review of different mobility models used for evaluating performance of routing protocols and applications designed for vehicular ad hoc networks. Particularly, it describes how accurate mobility traces can be built from a real-world car traffic dataset that embeds the main characteristics affecting vehicle-to-vehicle communications. An effective use of the proposed mobility models is illustrated in various road traffic conditions involving communicating vehicles equipped with 802.11p. This study shows that such dataset actually contains additional information that cannot completely be obtained with other analytical or simulated mobility models, while impacting the results of performance evaluation in vehicular ad hoc networks.

ESREL 2015 - European safety and reliability conference, Zürich, SUISSE, 07-/09/2015 - 10/09/2015; The integrity concept, safety quality criterion for satellite-based localisation systems used in aeronautics, is described in terms of levels (protection and alert levels), time (Time To Alarm) and probability (integrity risk). In land transport applications, the requirements in terms of integrity differ from aeronautics in their definition and values. Global Navigation Satellite Systems (GNSS) in railways suffer from additional weaknesses i.e. multipath and masking phenomena, which can degrade the localisation integrity. This situation cannot be tolerated in safety-related applications like train control and signalling. To mitigate these weaknesses, GNSS is usually combined with other localisation systems like inertial sensors. However, existing integrity monitoring processes are designed for GNSS integrity evaluation, i.e. to estimate the risk allocated to the position given by the GNSS receivers only. Our research work aims, first, to extend the integrity concept to such systems, and, secondly, to demonstrate how to evaluate, with this concept, the safety of a localisation system as expected in railways. The safety of GNSS-Based Localisation System is formalised and quantitatively evaluated.; Le concept d'intégrité, critère de sécurité pour les systèmes de localisation par satellite utilisés dans l'aéronautique, est décrite en termes de niveaux (niveaux de protection et d'alerte), le temps (temps d'alerte) et la probabilité (risque d'intégrité). Dans les applications de transport terrestre, les exigences en termes d'intégrité diffèrent de l'aéronautique dans leur définition et des valeurs. Les Global Navigation Satellite Systems (GNSS) dans le domaine ferroviaire souffrent de faiblesses supplémentaires telles que des phénomènes de multitrajets et de masquage, qui peuvent dégrader l'intégrité de la localisation. Cette situation ne peut être tolérée dans des applications liées à la sécurité, comme le contrôle/commande des trains et la signalisation. Pour atténuer ces faiblesses, le GNSS est généralement combiné avec d'autres systèmes de localisation comme des capteurs inertiels. Toutefois, les processus de surveillance de l'intégrité existants sont conçus pour l'évaluation de l'intégrité du GNSS, soit pour estimer le risque attribué à la position donnée par les récepteurs GNSS seulement. Notre travail de recherche vise, d'abord, à étendre le concept de l'intégrité de ces systèmes, et, d'autre part, à démontrer comment évaluer, avec ce concept, la sécurité d'un système de localisation comme attendu dans le domaine ferroviaire. La sécurité d'un système de localisation basé sur les GNSS est formalisée et quantitativement évaluée.

YRS 2015, Young reseachers seminar 2015, Rome, ITALIE, 17-/06/2015 - 19/06/2015; In this paper, we introduce a domain-specific component-based approach with traceability of concerns. It is based on the separation of concerns, which is a long well known fundamental principle of software engineering but some time neglected in practice. Our approach is included in the V-based development process prescribed by the CENELEC EN-50128 standard of railway control and protection systems. The core of our approach is a meta-model including traceability meta-model, which can be used to enable traceability of concerns within or across component-based system abstraction levels. We use the meta-model to design a small software part of RBC handover case study of ERTMS/ETCS. To demonstrate the consistency of this case study model and the impact of verification results on traceability links, we use a model-driven transformation approach to validate some requirements. The validation is formally achieved by using the UPPAAL model checker tool.

International Conference on Industrial Engineering and Systems Management, IESM 2015, Séville, Espagne, 21-/10/2015 - 23/10/2015; The study is based on an industrial expression pointing ausual way of performing a safety analysis: one consults the national railway accident database in order to evaluate the defense capacity of the system against scenarios of real past accidents.

European Rail Traffic Management System (ERTMS) is the standard control/command and signaling system implementing European railway operating rules. This standard aims to harmonize signaling and ensure interoperability in Europe using standard specification documents. The main issue is to model these rules and conduct formal verification and validation activities (V\&V) to tackle the complexity and criticality of these systems. Indeed, these specifications contain safety aspects based on permissions granted to roles to perform actions. Our approach is to model scenarios with role based formalisms, especially RBAC and Or-Bac and to transform them into B formal specifications in order to validate railway safety properties.; Le système européen de gestion du trafic ferroviaire (ERTMS) est un standard de contrôle/commande et de signalisation ferroviaire mettant en \oe{}uvre des règles européennes d'exploitation ferroviaires. Ce standard vise à harmoniser la signalisation et à assurer l'interopérabilité en Europe au moyen de documents standard de spécifications. La question principale que nous abordons est de pouvoir modéliser ces règles et de mener rigoureusement des activités de vérification et de validation formelles (V\&V) afin de faire face à la complexité et à la criticité de ces systèmes. En effet, ces spécifications contiennent des aspects de sécurité basés sur des autorisations accordées aux rôles pour effectuer des actions. Notre approche consiste à modéliser des scénarios avec des formalismes basés sur les rôles, notamment RBAC et Or-Bac et de les transformer en spécifications formelles B afin de valider les propriétés de sécurité ferroviaire.

The output of a system is always corrupted by additive noise, therefore it is more practical to develop estimation algorithms that are capable of handling noisy data. The effect of white additive noise has been widely studied, while a colored additive noise attracts less attention, especially for a continuous-time (CT) noise. Sampling issues of CT stochastic processes are reviewed in this thesis, several sampling schemes are presented. Estimation of a CT stochastic process is studied. An expectation-maximization-based (EM) method to CT autoregressive/autoregressive moving average model is developed, which gives accurate estimation over a large range of sampling interval. Estimation of CT Box-Jenkins models is also considered in this thesis, in which the noise part is modeled to improve the performance of plant model estimation. The proposed method for CT Box-Jenkins model identification is in a two-step and iterative framework. Two-step means the plant and noise models are estimated in a separate and alternate way, where in estimating each of them, the other is assumed to be fixed. More specifically, the plant is estimated by refined instrumental variable (RIV) method while the noise is estimated by EM algorithm. Iterative means that the proposed method repeats the estimation procedure several times until a optimal estimate is found. Many practical systems have inherent time-delay. The problem of identifying delayed systems are of great importance for analysis, prediction or control design. The presence of a unknown time-delay greatly complicates the parameter estimation problem, essentially because the model are not linear with respect to the time-delay. An approach to continuous-time model identification of time-delay systems, combining a numerical search algorithm for the delay with the RIV method for the dynamic has been developed in this thesis. In the proposed algorithm, the system parameters and time-delay are estimated reciprocally in a bootstrap manner. The time-delay is estimated by an adaptive gradient-based method, whereas the system parameters are estimated by the RIV method. Since numerical method is used in this algorithm, the bootstrap method is likely to converge to local optima, therefore a low-pass filter has been used to enlarge the convergence region for the time-delay. The performance of the proposed algorithms are evaluated by numerical examples; Cette thèse traite de l’identification de systèmes dynamiques à partir de données échantillonnées à pas variable. Ce type de données est souvent rencontré dans les domaines biomédical, environnemental, dans le cas des systèmes mécaniques où un échantillonnage angulaire est réalisé ou lorsque les données transitent sur un réseau. L’identification directe de modèles à temps continu est l’approche à privilégier lorsque les données disponibles sont échantillonnées à pas variable ; les paramètres des modèles à temps discret étant dépendants de la période d’échantillonnage. Dans une première partie, un estimateur optimal de type variable instrumentale est développé pour estimer les paramètres d’un modèle Box-Jenkins à temps continu. Ce dernier est itératif et présente l’avantage de fournir des estimées non biaisées lorsque le bruit de mesure est coloré et sa convergence est peu sensible au choix du vecteur de paramètres initial. Une difficulté majeure dans le cas où les données sont échantillonnées à pas variable concerne l’estimation de modèles de bruit de type AR et ARMA à temps continu (CAR et CARMA). Plusieurs estimateurs pour les modèles CAR et CARMA s’appuyant sur l’algorithme Espérance-Maximisation (EM) sont développés puis inclus dans l’estimateur complet de variable instrumentale optimale. Une version étendue au cas de l’identification en boucle fermée est également développée. Dans la deuxième partie de la thèse, un estimateur robuste pour l'identification de systèmes à retard est proposé. Cette classe de systèmes est très largement rencontrée en pratique et les méthodes disponibles ne peuvent pas traiter le cas de données échantillonnées à pas variable. Le retard n’est pas contraint à être un multiple de la période d’échantillonnage, contrairement à l’hypothèse traditionnelle dans le cas de modèles à temps discret. L’estimateur développé est de type bootstrap et combine la méthode de variable instrumentale itérative pour les paramètres de la fonction de transfert avec un algorithme numérique de type gradient pour estimer le retard. Un filtrage de type passe-bas est introduit pour élargir la région de convergence pour l’estimation du retard. Tous les estimateurs proposés sont inclus dans la boîte à outils logicielle CONTSID pour Matlab et sont évalués à l’aide de simulation de Monte-Carlo

10th FORMS-FORMAT symposium, Formal Methods for Automation and Safety in Railway and Automotive Systems, Braunschweig, ALLEMAGNE, 29-/09/2014 - 01/10/2014; This paper presents a high level Petri net modeling methodology for railway systems safety critical scenarios. This methodology is based on modular high level Petri nets, including most relevant components of a railway safety system, as safety regulation procedures, interlocking and especially human factors, enabling more various gathering of information and allowing the study of diverse possibilities in a same global model. At first, this method was applied to the infrastructure and the regulation of the Moroccan Kenitra railway station. Afterward, a first approach of real accident scenario modeling was introduced for 'Saint Romain en Gier' accident, taking account of human errors. Our goal is to bring formal tools in order to study weaknesses in shunting management within train stations and accidental scenarios, considering automatic mechanisms and human involvement.

1th International Symposium on Formal Aspects of Component Software , Bertinoro, Italie, 10-/09/2014 - 12/09/2015; International audience; One of the challenges that engineers face, during the development process of safety-critical systems, is the verification of safety application models before implementation. Formalization is important in order to verify that the design meets the specified safety requirements. In this paper, we formally describe the set of transformation rules, which are defined for the automatic transformation of safety application source models to timed automata target models. The source models are based on our domain-specific component model, named SARA, dedicated to SAfety-critical RAilway control applications. The target models are then used for the observer-based verification of safety requirements. This method provides an intuitive way of expressing system properties without requiring a significant knowledge of higher order logic and theorem proving, as required in most of existing approaches. An experimentation over a chosen benchmark at rail-road crossing protection application is shown to highlight the proposed approach.

Ce livrable (L3) décrit l’allocation de SIL par les trois méthodes les plus significatives identifiées dans le livrable 2 pour deux exemples de systèmes génériques (portes d’accès voyageurs et frein d’urgence). Dans un premier temps, ces trois méthodes et leur mise en pratique sont présentées brièvement. Ensuite, les deux cas concrets sont décrits et leurs fonctions de sécurité génériques sont identifiées. Sur la base de plusieurs situations dangereuses (SD) pouvant être engendrées par les deux sous-systèmes retenus, on procède à une répartition des objectifs de sécurité aux fonctions et aux sous-fonctions contribuant à chaque SD. On procède alors à l’allocation des SIL aux fonctions en mettant en ½uvre les méthodes identifiées. Une analyse et une comparaison des résultats obtenus sont présentées.

Railway operations management must cope with system failures and external disturbances that may cause delays. In heavy traffic areas, these delays can quickly propagate. This study details the results of a railway traffic optimization tool based on a MILP formulation. The case studies tackled represent different European locations. These experiments are part of a task the European FP7 project ON-TIME. The project aims to develop a prototype for a new generation of railway traffic management systems which will increase capacity and decrease delays for railway customers’ satisfaction.

Cyber Physical Systems (CPSs) are the next computing revolution and the new generation of complex System of Systems (SoSs). CPSs are complex and ubiquitous embedded devices coupled with global integration respecting Moore's Law. Therefore, to fit with their new characteristics, we are facing several challenges, such as the proliferation and the integration of these systems into scalable environment. A main concern of embedded real-time systems is safety. For such safety-critical systems, not only correct results count, but also the runtime duration for producing them. To ensure the dependability of such systems, which is not a local property of the system, but a global system property, the SoS safety has to be assessed, evaluated and checked according to its specific runtime context. In an attempt to address the challenges, we propose two domain specific languages for modeling the system architecture and the dynamic behaviour of heterogenous systems and their interactions. This paper shows how to develop an approach of real-time system design based on an extension of Milner's Calculus Communicating Systems since languages which are based on process algebra provide suitable features to formalise components communications.

International audience; Maintenance decisions can be directly affected by the introduction of a new asset on the market, especially when the new asset technology could increase the expected profit. However new technology has a high degree of uncertainty that must be considered such as, e.g., its appearance time on the market, the expected revenue and the purchase cost. In this way, maintenance optimization can be seen as an investment problem where the repair decision is an option for postponing a replacement decision in order to wait for a potential new asset. Technology investment decisions are usually based primarily on strategic parameters such as current probability and expected future benefits while maintenance decisions are based on “functional” parameters such as deterioration levels of the current system and associated maintenance costs. In this paper, we formulate a new combined mathematical optimization framework for taking into account both maintenance and replacement decisions when the new asset is subject to technological improvement. The decision problem is modelled as a non-stationary Markov decision process. Structural properties of the optimal policy and forecast horizon length are then derived in order to guarantee decision optimality and robustness over the infinite horizon. Finally, the performance of our model is highlighted through numerical examples.

This PhD thesis deals with fault diagnosis of DES in both untimed and timed contexts using Petri net models. Some on-the-fly and incremental techniques are developed to reduce the state explosion problem while analyzing diagnosability. In the untimed context, an algebraic representation for labeled Petri net (LPN) is developed to feature the system behavior. The diagnosability of LPN models is tackled by analyzing a series of K-diagnosability problems, where K is increased progressively. Two models called respectively FM-graph and FM-set tree are developed and built on the fly to record the necessary information for diagnosability analysis and online diagnosis. Finally, a diagnoser is derived from the FM-set tree for online diagnosis. In the timed context, time interval splitting techniques are developed in order to generate a state representation of labeled time Petri net models, for which techniques from the untimed context can be used to analyze diagnosability and perform online diagnosis. Based on this, necessary and sufficient conditions for the diagnosability of LTPN models are determined. Moreover, we provide the solution for the minimum delay that ensures diagnosability. From a practical point of view, diagnosability analysis is performed on the basis of on-the-fly building of a structure that we call ASG and which holds fault information about the LTPN states. Generally, using on-the-fly analysis and incremental techniques makes it possible to build and investigate only a part of the state space. Analysis results obtained on some chosen benchmarks show the efficiency in terms of time and memory compared with the traditional approaches based on state enumeration.; Cette thèse s'intéresse à l'étude des problèmes de diagnostic des fautes sur les systèmes à événements discrets dans des contextes atemporel et temporel sur la base de modèles réseau de Petri. Des techniques d'exploration incrémentale et à-la-volée sont développées pour combattre le problème de l'explosion de l'espace d'état. Dans le contexte atemporel, une représentation algébrique pour les réseaux de Petri labellisés (RdP-L) a été développée pour caractériser le comportement du système. La diagnosticabilité de modèles RdP-L est ensuite abordée par l'analyse d'une série de problèmes d'analyse de K -diagnosticabilité, où K peut être augmenté progressivement. Concrètement, l'analyse de la diagnosticabilité est effectuée sur la base de deux modèles nommés respectivement FM-graph et FM-set tree qui sont développés à-la-volée et qui contiennent les informations relatives aux fautes. Un diagnostiqueur peut facilement être dérivé à partir du FM-set tree pour le diagnostic en ligne. Dans le contexte temporel, une technique de fractionnement des intervalles de temps a été élaborée pour développer une représentation de l'espace d'état des réseaux de Petri labellisés et temporels (RdP-LT) pour laquelle des techniques d'analyse de la diagnosticabilité du contexte atemporel, peuvent être exploitées. Sur cette base, les conditions nécessaires et suffisantes pour la diagnosticabilité de RdP-LT ont été déterminées, et nous présentons la solution pour le délai minimum qui assure la diagnosticabilité. En pratique, l'analyse de la diagnosticabilité est effectuée sur la base de la construction à-la-volée d'une structure que l'on appelle ASG et qui contient des informations relatives à l'occurrence de fautes sur les états du RdP-LT. D'une manière générale, l'analyse effectuée sur la base des techniques à-la-volée et incrémentale permet de construire et explorer seulement une partie de l'espace d'état. Les résultats des analyses effectuées sur certains benchmarks montrent l'efficacité des techniques que nous avons développées en termes de temps et de mémoire par rapport aux approches traditionnelles basées sur l'énumération des états.

This PhD thesis deals with fault diagnosis of DES in both untimed and timed contexts using Petri net models. Some on-the-fly and incremental techniques are developed to reduce the state explosion problem while analyzing diagnosability. In the untimed context, an algebraic representation for labeled Petri net (LPN) is developed to feature the system behavior. The diagnosability of LPN models is tackled by analyzing a series of K-diagnosability problems, where K is increased progressively. Two models called respectively FM-graph and FM-set tree are developed and built on the fly to record the necessary information for diagnosability analysis and online diagnosis. Finally, a diagnoser is derived from the FM-set tree for online diagnosis. In the timed context, time interval splitting techniques are developed in order to generate a state representation of labeled time Petri net models, for which techniques from the untimed context can be used to analyze diagnosability and perform online diagnosis. Based on this, necessary and sufficient conditions for the diagnosability of LTPN models are determined. Moreover, we provide the solution for the minimum delay that ensures diagnosability. From a practical point of view, diagnosability analysis is performed on the basis of on-the-fly building of a structure that we call ASG and which holds fault information about the LTPN states. Generally, using on-the-fly analysis and incremental techniques makes it possible to build and investigate only a part of the state space. Analysis results obtained on some chosen benchmarks show the efficiency in terms of time and memory compared with the traditional approaches based on state enumeration., Cette thèse s'intéresse à l'étude des problèmes de diagnostic des fautes sur les systèmes à événements discrets dans des contextes atemporel et temporel sur la base de modèles réseau de Petri. Des techniques d'exploration incrémentale et à-la-volée sont développées pour combattre le problème de l'explosion de l'espace d'état. Dans le contexte atemporel, une représentation algébrique pour les réseaux de Petri labellisés (RdP-L) a été développée pour caractériser le comportement du système. La diagnosticabilité de modèles RdP-L est ensuite abordée par l'analyse d'une série de problèmes d'analyse de K -diagnosticabilité, où K peut être augmenté progressivement. Concrètement, l'analyse de la diagnosticabilité est effectuée sur la base de deux modèles nommés respectivement FM-graph et FM-set tree qui sont développés à-la-volée et qui contiennent les informations relatives aux fautes. Un diagnostiqueur peut facilement être dérivé à partir du FM-set tree pour le diagnostic en ligne. Dans le contexte temporel, une technique de fractionnement des intervalles de temps a été élaborée pour développer une représentation de l'espace d'état des réseaux de Petri labellisés et temporels (RdP-LT) pour laquelle des techniques d'analyse de la diagnosticabilité du contexte atemporel, peuvent être exploitées. Sur cette base, les conditions nécessaires et suffisantes pour la diagnosticabilité de RdP-LT ont été déterminées, et nous présentons la solution pour le délai minimum qui assure la diagnosticabilité. En pratique, l'analyse de la diagnosticabilité est effectuée sur la base de la construction à-la-volée d'une structure que l'on appelle ASG et qui contient des informations relatives à l'occurrence de fautes sur les états du RdP-LT. D'une manière générale, l'analyse effectuée sur la base des techniques à-la-volée et incrémentale permet de construire et explorer seulement une partie de l'espace d'état. Les résultats des analyses effectuées sur certains benchmarks montrent l'efficacité des techniques que nous avons développées en termes de temps et de mémoire par rapport aux approches traditionnelles basées sur l'énumération des états.

La modélisation est un processus dédié à l'analyse des exigences dans le but de formaliser les représentations informelles des exigences système. La vérification, en revanche, est un processus de qualification qui permet de détecter et prévenir les défaillances dans les modèles. Ces deux approches sont de plus en plus utilisées dans l'industrie pour maîtriser la complexité croissante des systèmes conçus. Le papier propose une méthodologie générale de modélisation et de vérification pour les systèmes de contrôle à temps réel en se basant sur la ré-utilisabilité des connaissances des experts du domaine pour favoriser les échanges entre les projets similaires. Le papier présente une architecture d'une plate-forme dédiée à l'évaluation des systèmes basée sur un modèle générique de référence des systèmes de contrôle à temps-réel.

L’interopérabilité est un paramètre clef pour la compétitivité des systèmes ferroviaires européens. Elle est la condition à l’ouverture de nouveaux marchés et à la mise à disposition de nouveaux services. Un des points critique et la faculté de délivrer un service performant et sûr, sans avoir recours à des transbordements de passagers ou de matériels. Une des étapes est le respect d’un ensemble de règlements techniques opérationnels qui garantissent que les exigences essentielles sont vérifiées. Le projet Perfect veut contribuer à la validation d’une implantation des spécifications européennes d’interopérabilité sur le sol français. Concrètement, ERTMS " European Rail Traffic Management System ", ne définit que l’environnent technique et opérationnel des matériel à bord des trains. Le comportement des matériels au sol est pour sa part essentiellement régi par les lois nationales. Ce dernier aspect produit une certaine complexité dans l’analyse de sécurité du système global. La proposition principale du projet est d’étudier la consistance des différentes spécifications entre elles en utilisant des outils formels et en choisissant l’angle de la sécurité. Ce problème, critique au regard des enjeux, n’est abordé dans la littérature que de manière très parcellaire.

Evaluating dependability of complex systems requires the evolution of the system states over time to be analysed. The problem is to develop modelling approaches that take adequately the evolution of the different operating and failed states of the system components into account. The Fault Tree (FT) is a well-known method that efficiently analyse the failure causes of a system and serves for reliability and availability evaluations. As FT are not adapted to dynamic systems with repairable multi-state components, extensions of FT (eFT) have been developed. However efficient quantitative evaluation processes of eFT are missing. Petri nets have the advantage of allowing such evaluation but their construction is difficult to manage and their simulation performances are unsatisfactory. Therefore, we propose in this paper a new powerful process to analyse quantitatively eFT. This is based on the use of PN method, which relies on the failed states highlighted by the eFT, combined with a new analytical modelling approach for critical events that depend on time duration. The performances of the new process are demonstrated through a theoretical example of eFT and the practical use of the method is shown on a satellite-based railway system.

les travaux de recherche détaillés dans le manuscrit portent sur des aspects relatifs à la sécurité des systèmes complexes de contrôle/commande, avec des applications dans le domaine ferroviaire. Les contributions sont présentées selon deux axes : 1. L'axe Ingénierie des exigences, et notamment l'étape de spécification qui consiste à exprimer les contraintes, propriétés et règles que le système doit satisfaire . 2. L'axe Surveillance, et en particulier les activités de détection et diagnostic dont l'objectif est d'assurer le suivi du comportement du système, et déceler et identifier les éventuels dysfonctionnements The research work discussed is relative to safety of control/command complex systems with various applications in the railway domain. The results are discussed through two main directions: 1. Requirements' engineering, and particularly the specification step which consists in expressing constraints, properties and rules the system must satisfy: This step is crucial while engineering a complex system especially when the system shows a high criticality level. Actually, the quality of specifications impacts several subsequent steps in the system development cycle. The work developed w.r.t. these aspects offer contributions in terms of refinement/formalization of the requirements expressed in informal and semi-formal shapes and relative to critical systems. The rigor level of the obtained formulations is such that using formal methods for the verification/validation phase becomes systematic. 2. Monitoring and in particular detection and diagnosis activities of which the goal is to ensure behavior supervision and to detect and identify possible failures: In general, diagnosis techniques can be classified according to various criteria, among which whether a behavioural model is used and which kind of model. Here, we consider a context where the system behavior is depicted by a state/transition model (automaton, Petri nets, etc.). Indeed, in a sufficiently high abstraction level, discrete models offer a convenient basis for monitoring activities. In this context, two main issues have to be dealt with: diagnosability which ensures that each failure (or failure class) can be detected and identified within a finite delay upon its occurrence, and the establishment of a diagnoser which performs online monitoring of the system behavior. In this manuscript three major contributions pertaining to diagnosis are discussed. The first contribution considers a Labeled Petri Net (LPN) model for the behavior description and advocates the use of incremental and on-the-fly exploration of the system state space to assess diagnosability and develop online diagnosers. Some experimentations through various benchmarks have been carried out, and the obtained results show a good efficiency in terms of time and memory saving relatively to some main DES diagnosis approaches based on exhaustive exploration of the state space. The second contribution considers a timed context while taking a Labeled Time Petri Net (LTPN) model of the system. A technique based on time interval splitting has been developed, thus making it possible to adopt the results obtained for diagnosis in untimed context to deal with the diagnosis issues in timed context. Diagnosability analysis is performed on the basis of the state class graph of the LTPN, and the online diagnoser can be generated in a straightforward way. The third contribution pertaining to the diagnosis topic consists in developing an operative logical formulation, i.e. a formulation that can be executed in a direct way, of the diagnosability property. Concretely, diagnosability investigation is performed by computing a sequence of logical µ-calculus relations. The advantage of such a formulation is that it offers a single homogeneous logical framework to deal with the main diagnosis issues, while making it possible to use model-checking technique to deal with such questions. We also show that the developed formulation offers good flexibility. Different case studies, mainly related to railway control/command, are given to illustrate the various contributions.

This work focuses on modeling and simulating the behavior of a real-time control system using the Goal Oriented Requirement Engineering approach and Discrete Event System Specification formalism for Realtime. This is the first attempt to combine the goal-based approach with a model of discrete event system to check the safety properties of a real-time control system. In order to bring more insight into the goal-based model and the behavior-based model, we illustrate our methodology by an example of the air traffic control system. To improve the decision making in the modeling process and to remove fault risk from the designing process, a simulation driven by a multi-agent systems is provided.

The modeling process aims to define and analyse requirements for testing physical scale systems such as robotic surgery machines, railway signalling and control systems, nuclear reactor control systems, etc... These safety-critical systems whose failure may result in severe human or physical damage, are designed to be testable and verifiable before their implementation. To understand the system specifications and its functionalities, different types of models are used and each one reflects a viewpoint of a particular scope. Furthermore, its aim is to risk analysis and performance testing. Our approach is based on goal-oriented requirements elicitation, structuring and analysis. To automate the latter requirements engineering processes it is crucial that we involve expert knowledge. This process needs to be split into several steps. This work is limited to present techniques to obtain specifications dependency graphs from a set of requirements to determine the global goal model. This paper presents a domain independent framework for operational requirements modeling beside of specifications structuring technique based on Guidance Ontology. The present work focuses on improving the performance of structuring techniques through a pattern recognition based on a guidance ontology. This approach is shown to enable the structuring process automation by making use of domain ontologies as an expert knowledge base and capitalization.

This paper deals with the active robustness of a milk manufacturing workshop including time interval constraints. Such systems have robustness properties towards time disturbances. The robustness property can be a static property, but using a dynamic control strategy may increase the robustness value. Controlled P-time Petri nets are used as a modelling tool. Some definitions and a series of lemmas are cited in order to build a theory dealing with robustness problems. In order to avoid the death of marks at the synchronisation transitions of the P-time Petri net model, a robust control strategy facing time disturbances is presented. The proposed approach tries to reject the disturbance as soon as it is observed. Furthermore, this approach is used by an algorithm computing an active robustness margin at a given node. It is illustrated step by step on an example of a milk manufacturing workshop. A comparison with the bound provided for the passive robustness is made.

In the context of safety requirement engineering, model transformation is a task of interest. Indeed, it allows us to keep all the requirements while switching from one point of view to another. The presented work assumes that a valid solution has been found and proposes an approach in order to build a valid implementation. As some fine dynamic properties are integrated into the specification, high-level Petri nets are used to specify and verify the solution. Then, considering an industrial railway context, the transformation of the Petri net model in order to provide an input to a B process is considered. This last consideration leads to a proposition of a systematic direct transformation of the Petri net model into abstract B machines. The approach is illustrated by a theoretical railway example. The limitations of this approach are discussed at the end of the paper and some prospects are detailed.

Air and rail transportation systems are characterized by important common features: they serve a significant share of passenger traffic in Europe; their functioning relies on the cooperation of many stakeholders operating a fixed timetable, often with competing objectives; and they have been characterized by quite a fragmented development following national borders. For these systems, the European Commission envisages a common future in terms of an increase of efficiency and elimination of national borders. In this paper, we analyze the two systems in the perspective of their common development and we underline the main existing differences linked to the management of the infrastructure. These differences concern the processes implemented for specifying and allocating capacity, both in strategic planning and in real-time intervention. Our analysis suggests that the air transportation system is moving in the direction indicated by the European Commission, as well as the rail transportation system for what concerns international train paths (typically high-speed trains). However, a substantial separation still exists between conventional rail transportation systems of different countries.

The quantification and characterisation of hydrological and sedimentary transfers are now major challenges, not only in terms of knowledge of hydrosystems way of functioning, but also for the management of the environment and its natural resources. Indeed, the consequences associated with these transfers can be catastrophic for land ecosystems and aquatic biodiversity as well as for people, when they are accompanied by transfers of pollutants, flooding or pollution. These are so many issues critical to preserving and restoring water resources and soils that are now one of the government's environmental priorities (Law on Water; Water Framework Directive, WFD). While there are questions on watercourse and watersheds managements, we conducted a study focussed on typical feature for low-energy water system (, L'élaboration de la Directive Cadre sur l'Eau (DCE) en 2000 et de la Loi sur l'Eau et les Milieux Aquatiques (LEMA) en 2006 a mis en lumière l'importance de la quantification et de la caractérisation des transferts hydrosédimentaires dans les cours d'eau pour la gestion des milieux et des ressources naturelles. En effet, les conséquences associées à ces transferts peuvent être catastrophiques pour les écosystèmes continentaux et aquatiques, la biodiversité et même pour les populations (inondations, pollutions). A l'heure où l'on s'interroge sur les modalités de gestion des masses d'eau et des bassins versants, nous avons mené une étude centrée sur les cours d'eau " ordinaires " de l'ouest de la France, qui disposent généralement d'une énergie réduite (

During the last decades, various techniques have been developed to deal with diagnosis issues on Discrete Event Systems (DES). These techniques, even if they have reached a good maturity degree, need the elaboration of intermediate ad-hoc models from the original model, in order to proceed to diagnosability investigation. Instead of developing ad-hoc products between models, we have suggested a new formulation of DES diagnosability issue using a unique logical framework, μ-calculus. Therefore, diagnosability analysis is performed through the computing of successive logical relations. In this paper, a brief overview of this formulation is given, then we develop an original implementation of diagnosability investigation on the basis of the formulation. Our implementation consists of a DBMS-architecture (Database Management System) where system behavior is encoded as a set of relational tables and where diagnosability investigation is performed through an ordered sequence of queries on these tables. With this successful prototype implementation, we are confident to pave the way for applying the method on real-size systems while taking advantage of the performances of new DBMS inference engines, the decentralization facilities on DBMS and of new technologies for external storing hardware. To our knowledge, this is the first work that employs a DBMS architecture to perform diagnosability analysis on DES.

Systems? requirements are usually written in a natural language since it generally means a greater understanding among the various stakeholders. However, using an informal language potentially gives rise to interpretation problems, which are to be resolved prior to using (automated) verification techniques. This article tackles an important issue pertaining to requirement engineering: how to guide and help requirements? formalization? In order to support the formalization process, we propose a methodology based on a formal structure, which is the corner stone of the refinement process. The operating mode of the refinement process is highly iterative: the aforementioned structure is constructed incrementally until its validity is formally obtained. Although this process is formally backed up, it is a fundamentally subjective one, which means that interpretation errors can still occur. In case of errors, it is essential to be able to backtrack refinements until an interpretation error is found. This is why we require that each refinement be associated with a justification which may subsequently be analyzed in case an error occurred during the verification phase. This formalization process was designed to be used alongside an (unspecific) engineering process, in charge of the implementation. Once the formalization is complete, it is checked against the implementation using testing techniques, or directly against an implementation model via model-checking.

International audience; Cet article propose une méthode originale pour la conception à moindre coût de systèmes d'automatisation tolérants aux fautes. La sûreté de fonctionnement est évaluée de manière semi-quantitative en tenant compte de l'ordre d'apparition des défaillances. Cette évaluation tient compte du nombre, de l'ordre et de la longueur des séquences menant aux événements redoutés. Cette méthode présente l'intérêt d'être suffisamment simple pour permettre d'étudier un grand nombre de solutions potentielles d'architectures matérielles et suffisamment précise pour permettre leur comparaison. Parmi les méthodes d'évaluation classiques, certaines permettent de traiter cet aspect dynamique (graphe de Markov, réseau de Petri), mais elles ne sont pas ou peu appropriées pour la comparaison de différentes solutions. La méthode de conception présentée y remedie par l'emploi d'alternatives de réalisation. Une phase d'optimisation vient sélectionner les meilleures alternatives en maximisant la sûreté de fonctionnement pour un coût donné. La méthode est illustrée par la conception d'un système de détection des incendies pour le ferroutage.

International audience; In recent years, image-processing solutions have been to automatically detect incidents and make measurements on video images from CCTV cameras, relieving the staff in control rooms of much of the difficulty in finding out where events that require attention are occurring. In this paper we illustrate some of the results obtained with on-site experiments carried out as part of projects funded by the European Commission and some additional experimentation carried out outside the project. We present here details on the systems, algorithms and their performance evaluation. Three different specific events in transport networks are described: abnormal stationarity, queuing, intrusion detection and loitering. Promising results are obtained from onsite experimentation

Les travaux de recherche présentés dans cette thèse s'intéressent à la conception de systèmes complexes d'automatisation sûrs de fonctionnement. L'évaluation semi-qualitative de la sûreté de fonctionnement est basée sur l'étude de différents scénarios menant à des événements redoutés. Pour déterminer une architecture matérielle optimale, il est important de disposer d'outils de modélisation et d'évaluation rapides ainsi que d'algorithmes d'optimisation adaptés au sein d'une méthodologie globale de conception. Cette méthodologie doit permettre d'étudier l'impact des défaillances sur le comportement final du système contrôlé. La méthode repose sur une modélisation fonctionnelle et une modélisation dysfonctionnelle utilisant les scénarios de modes de défaillances. Nous proposons une représentation graphique baptisée Arbre de défaillances multiples amélioré permettant de modéliser, à l'aide d'opérateurs temporels et de relations entre modes de défaillances, l'ensemble des comportements dysfonctionnels. Ce modèle permet de plus de décrire différentes possibilités d'agencements des composants utilisables ainsi que plusieurs types de composants, possédant par exemple des niveaux de robustesse différents vis-à-vis des défaillances. En appliquant une méthode d'optimisation de type Branch and Bound en prenant comme critères la longueur minimale des scénarios et le nombre de combinaisons de scénarios, nous obtenons un ensemble d'architectures matérielles de coût minimal pour un niveau de sûreté donné. La méthodologie est ensuite appliquée à la conception d'un wagon instrumenté pour le ferroutage. Les fonctionnalités considérées pour le wagon dît intelligent concernent les détections de l'incendie et du désarrimage. L'intégration de ces travaux dans un logiciel dédié à la conception de systèmes d'automatisation (plate-forme ALoCSyS : Atelier Logiciel de Conception de Systèmes Sûrs) est décrite. Thèse sous la direction de HAYAT,S (INRETS-ESTAS), COCOMPOT,V et CONRARD,B

Our work is dedicated to the modeling and the analysis of concurrent and distributed systems. More precisely, we seek to model, verify and supervise systems composed by autonomous entities which interact locally through shared memory and globally through asynchronous message passing. In this context, we argue that, instead of modeling each entity independently and then analyzing what happens when all of them interact, it is better tohave a complete theory to globally describe a concurrent system, in which verification and supervision analysis are decidable. This theory is based on partially ordered multisets (ie. “pomsets”) which is a “true-concurrency” model. To this end, we defined the causal hmsc model, based on pomsets and which extends the standardized hmsc formalism with constructs from Mazurkiewicz trace theory. We first show that a syntactic restriction of causal hmsc is equivalent to bounded mixed automata, a formalism which extends Zielonka asynchronous automata and communicating finite state machines. We also show that classical model-checking techniques can be extended to pomsets-based formalisms without losing efficacy. This is an important result, as pomsets-based formalisms, such as causal hmsc, are more concise than sequential system formalisms. Finally, we propose efficient methods to analyse large recorded files from distributed executions and we propose supervision techniques such as diagnosis and event correlation, using pomsets-based models of distributed and concurrent systems.; Cette thèse se place dans le cadre de la modélisation et de l'analyse de systèmes parallèles et répartis. Plus précisément, nous nous intéressons à la modélisation, la vérification et la supervision de systèmes, composés d'entités indépendantes interagissant localement par mémoire partagée et globalement par échange asynchrone de messages.Dans ce contexte, plutôt que de modéliser séparément chaque entité, puis d'analyser les comportements qui peuvent se produire lorsque ces entités interagissent, nous fournissons une théorie permettant de modéliser globalement le système considéré tout en conservant des propriétés de vérification et de supervision décidables. Cette théorie se base sur le formalisme des ordres partiels étiquetés (appelés "pomsets").Dans ce but, nous définissons le modèle des HMSC causaux qui étend le formalisme des HMSC en autorisant, comme pour les traces de Mazurkiewicz, certains événements à commuter sur chaque processus. Nous montrons, tout d'abord, qu'une restriction syntaxique des HMSC causaux a le même pouvoir d'expression que les réseaux bornés d'automates mixtes, un modèle qui étend les réseaux d'automates asynchrones de Zielonka et les réseaux d'automates communicants. De plus, nous montrons que les méthodes classiques de model-checking de systèmes séquentiels peuvent s'appliquer aux modèles plus concis basés sur les pomsets, comme les HMSC causaux, sans perte d'efficacité. Enfin, nous proposons des méthodes de traitement efficace d'observations volumineuses d'exécutions réparties, ainsi que des techniques de supervision, telles que le diagnostic ou la corrélation d'événements, qui utilisent des modèles basés sur les pomsets.

Cet article a pour principal objectif l’analyse d’un système afin d’estimer et d’évaluer la performance de celui-ci. La notion de système complexe y est largement décrite, vue structurelle ou statique, vue temporelle ou dynamique, etc. Les notions de erformance de système et de mesure de cette performance sont elles aussi définies. Différentes méthodes d’analyse (techniques et fonctionnelles) permettent la description et la représentation du fonctionnement du système, dont la gestion de l’incertitude (vue probabiliste et possibiliste) ne peut être écartée. Les méthodes d’évaluation de la sûreté de fonctionnement viennent en conclusion de cet article