284 research outputs found
Analysis and formal specification of relay-based railway interlocking systems
No full textLes Systèmes d'Enclenchement Ferroviaire (SEF) basés sur des relais sont des systèmes critiques, ils doivent être spécifiés et leur sécurité doit être prouvée afin de garantir l'absence de dangers lors de leurs exécutions. Toutefois, il s'agit d'une tâche difficile, car les SEF à relais ne sont généralement modélisés que de manière structurelle, de sorte que leur analyse comportementale est effectuée manuellement sur la base des connaissances des experts sur le système. Cependant, l'existence d'une description formelle du comportement des SEF est impérative pour pouvoir effectuer des preuves de sécurité. En outre, comme les SEF informatisés ont tendance à être moins chers, plus faciles à entretenir et à faire évoluer, le secteur ferroviaire a intérêt à ce qu'il existe une méthodologie pour transformer des SEF à relais existants en SEF informatisés.Les méthodologies formelles de spécification sont fondées sur des bases mathématiques solides qui permettent de prouver la sécurité des systèmes. En outre, de nombreux langages de spécification formelle prennent en charge non seulement la vérification, mais aussi la mise en œuvre de ces systèmes par un processus de développement formalisé. Ainsi, les méthodes formelles peuvent être la clé pour prouver la sécurité des SEF et les mettre en œuvre en utilisant des technologies informatiques.Cette thèse aborde deux propositions principales. Premièrement, elle présente une analyse des informations des diagrammes à relais et de la formalisation de la structure et du comportement des SEF basés sur des expressions mathématiques afin de créer un certain niveau de formalisation des systèmes. Le modèle résultant peut être étendu et adapté afin de se conformer à différents contextes ferroviaires et il peut aussi être utilisé afin de soutenir la spécification de ces systèmes dans différents langages de spécification formels. Ensuite, cette thèse présente comment le modèle formel des SEF peut être adapté afin de spécifier formellement ces systèmes selon la méthode B, un langage de spécification formel qui a déjà été utilisé avec succès dans le domaine ferroviaire et qui permet de prouver la sécurité du système et de le mettre en œuvre en tant que système informatique.En définitive, cette thèse présente une méthodologie complète pour la spécification et la vérification des Systèmes d'Enclenchement Ferroviaire basés sur des relais, en fournissant un support pour la preuve des systèmes dans différents contextes et pour leur spécification et leur mise en œuvre dans de nombreux langages formels différents.Relay-based Railway Interlocking Systems (RIS) are critical systems and must be specified and safety proved in order to guarantee the absence of hazards during their execution. However, this is a challenging task, since Relay-based RIS are generally only structurally modelled in a way that their behavioural analysis are made manually based on the experts knowledge about the system. Thus, the existence of a RIS behavioural formal description is imperative in order to be able to perform safety proofs. Furthermore, as Computer-based RIS tend to be less expensive, more maintainable and extendable, the industry has interest in the existence of a methodology for transforming the existing Relay-based RIS into Computer-based RIS.Formal specification methodologies are grounded in strong mathematical foundations that allow the systems safety proof. Besides, many formal specification languages support not only the verification, but also the implementation of these systems through a formal development process. Thus, Formal Methods may be the key in order to prove the RIS safety and implement them with computer-based technologies.This thesis addresses two main propositions. Firstly, it presents an analysis of the relay diagrams information and a formalisation of the Relay-based RIS structure and behaviour based on mathematical expressions as a way to create a certain level of formalisation of the systems. The resulting model can be extended and adapted in order to conform to different railway contexts and it can be used in order to support the specification of these systems in different formal specification languages. Then, this thesis presents how the RIS formal model can be adapted in order to formally specify these systems in B-method, a formal specification language with a successful history in the railway field and which allows the system safety proof and implementation as computer-based systems.As a result, this thesis presents a complete methodology for the specification and verification of Relay-based Railway Interlocking Systems, giving support for the systems safety proof in different contexts and for their specification and implementation in many different formal languages
A Vision of Intelligent Train Control
No full textThe progressive adoption of artificial intelligence and advanced communication technologies within railway control and automation has brought up a huge potential in terms of optimisation, learning and adaptation, due to the so-called “self-x” capabilities; however, it has also raised several dependability concerns due to the lack of measurable trust that is needed for certification purposes. In this paper, we provide a vision of future train control that builds upon existing automatic train operation, protection, and supervision paradigms. We will define the basic concepts for autonomous driving in digital railways, and summarise its feasibility in terms of challenges and opportunities, including explainability, autonomic computing, and digital twins. Due to the clear architectural distinction, automatic train protection can act as a safety envelope for intelligent operation to optimise energy, comfort, and capacity, while intelligent protection based on signal recognition and obstacle detection can improve safety through advanced driving assistance
Safe and Time-Optimal Control for Railway Games
No full textRailway scheduling is a complex and safety critical problem that has recently attracted attention in the formal verification community. We provide a formal model of railway scheduling as a stochastic timed game and using the tool Uppaal Stratego, we synthesise the most permissive control strategy for operating the lights and points at the railway scenario such that we guarantee system's safety (avoidance of train collisions). Among all such safe strategies, we then select (with the help of reinforcement learning) a concrete strategy that minimizes the time needed to move all trains to their target locations. This optimizes the speed and capacity of a railway system and advances the current state-of-the-art where the optimality criteria were not considered yet. We successfully demonstrate our approach on the models of two Danish railway stations, and discuss the applicability and scalability of our approach
Safety Analysis of Automatic Train Operation Based on ETCS
No full textIn Germany and throughout Europe, train operation using the European Train Control System (ETCS) is the most common solution for current trains running on the mainlines. This paper presents a safety analysis of the Automatic Train Operation (ATO) system. The System Modeling Language (SysML) is used to visually model the logical relationships of the mainline ATO system based on ETCS. The Failure Mode and Effect Analysis (FMEA) is used to perform a qualitative safety analysis to identify all possible failure modes of the system. State-space modeling and dynamic quantitative analysis are carried out using a Markov chain model. In order to verify the degree of safety of the ATO model, a real data set from a train operator was used for simulation. We show that using an ETCS-based ATO system to control trains can achieve higher reliability on the mainline with less maintenance than if experienced drivers control trains.</p
Towards a modular architecture of formal modelling : system/sub-systems decomposition in event-B
No full textLes activités d’analyse et de modélisation des systèmes critiques, tels que les systèmes ferroviaires, constituent des tâches d’envergure nécessitant des mécanismes rigoureux. Fondées sur des bases mathématiques, les méthodes formelles peuvent aider à mener rigoureusement ces activités et à réduire l'ambiguïté des spécificités de ces systèmes. La méthode B événementiel fait partie des méthodes les plus utilisées et recommandées pour la modélisation système. Le mécanisme central d’une modélisation système en B événementiel est le raffinement. En effet, le raffinement consiste à détailler des spécifications abstraites afin d'obtenir des spécifications plus concrètes. En outre, le processus de raffinement doit être prouvé afin d'assurer la cohérence et la correction de la modélisation du système entre deux niveaux de raffinement. Bien que la méthode B événementiel dispose d’un mécanisme de raffinement permettant de passer d’un niveau abstrait à un niveau de granularité plus fine, les modèles formels pour de tels systèmes sont souvent complexes et volumineux. En outre, il est difficile de communiquer autour de ces modèles entre les différents corps de métier (les experts métier du domaine, les ingénieurs système, les ingénieurs sous-systèmes, etc.) et de gérer les différentes briques du système fournies. Ceci nécessite, dans la majorité des cas, une intervention manuelle assurant la synergie entre ces acteurs.Dans le but d’avoir une meilleure communication et gestion, la décomposition est apparue comme technique qui complète le raffinement. Ce mécanisme a pour but de diminuer la complexité du modèle initial en le partitionnant en sous-modèles, et de faciliter par conséquent les activités de vérification formelle. Les approches de décomposition proposées dans la littérature ont quelques limitations au vu des besoins industriels exprimés dans le cadre des systèmes critiques, entre autres, le raisonnement système/sous-systèmes. L’application de ces approches sur de tels systèmes est particulièrement difficile et exige des étapes intermédiaires de raffinement. En effet, ces méthodes de décomposition peuvent entraîner une perte de quelques propriétés du système comme les propriétés de sécurité ou une incohérence du comportement exprimé dans les sous-modèles avec celui du modèle initial.Sur la base de cette problématique, le sujet de thèse est focalisé sur la définition d’une nouvelle approche modulaire de modélisation des systèmes critiques basée sur la décomposition en B événementiel. Cette approche porte sur la décomposition d’un système en plusieurs sous-systèmes en préservant le comportement du système global. Cela est assuré par la définition de nouveaux liens sémantiques ainsi que de nouvelles règles pour la génération des obligations de preuve associées. La correction de l’approche proposée est assurée en démontrant que l’ensemble des composants résultants, après la décomposition, constitue un raffinement du système initial décomposé. Cette méthodologie est illustrée par un cas d’étude concret issu du secteur ferroviaireThe activities of analysis and modelling of critical systems, such as railway systems, are large-scale tasks requiring rigorous mechanisms. Founded on mathematical bases, formal methods can help to rigorously conduct these activities and reduce the ambiguity of the specifics of these systems. The Event-B method is one of the most widely used and recommended methods for system modelling. The central mechanism of Event-B system modelling is refinement. Indeed, the refinement consists in detailing abstract specifications in order to obtain more concrete specifications. In addition, the refinement process must be proven in order to ensure consistency and correctness of the system modelling between two levels of refinement. Although the Event-B method has a refinement mechanism to move from an abstract level to a finer level of granularity, the formal models for such systems are often complex and large. In addition, it is difficult to communicate around these models between the different trades (business experts in the field, system engineers, subsystems engineers, etc.) and to manage the different provided bricks of the system. This requires, in the majority of cases, a manual intervention ensuring the synergy between these actors.In order to have better communication and management, the decomposition has emerged as a technique that complements refinement. This mechanism aims to reduce the complexity of the initial model by its partitioning into sub-models, and consequently to facilitate formal verification activities. In the literature, the proposed decomposition approaches have some limitations regarding the industrial needs expressed in the context of critical systems, among others, system/sub-systems reasoning. The application of these approaches on such systems is particularly difficult and requires intermediate stages of refinement. Indeed, these decomposition methods can lead to a loss of some properties of the system such as security properties and/or an inconsistency of the behaviour expressed in the sub-models with that of the initial model.On the basis of this problematic, the thesis subject is focused on the definition of a new modular approach for modelling critical systems based on the Event-B decomposition. This approach focuses on the decomposition of a system into several sub-systems while preserving the behaviour of the overall system. This is ensured by the definition of new semantic links as well as new rules for the generation of the associated proof obligations. The correctness of the proposed approach is ensured by demonstrating that the set of resulting components, after decomposition, constitutes a refinement of the initial decomposed system. This methodology is illustrated by a concrete case study from the rail secto
Ontologies for railway safety management : integration of the dysfunctional analysis into the design
No full textLa sécurité-innocuité est une propriété émergente des systèmes critiques de sécurité (SCS), notamment les systèmes ferroviaires. Cet aspect émergent complexifie leur processus du développement et nécessite un raisonnement judicieux permettant de diminuer les dangers. Cette thèse propose une approche ontologique qui intègre les activités de sécurité dès les premières phases de conception des SCS. Ce cadre structuré offre une harmonisation sémantique entre les domaines impliqués, tels que l'ingénierie de sécurité et l'Ingénierie des Exigences Dirigée par les Buts (IEDB). La logique métier intégrée dans cette approche est validée par des cas d'étude ferroviaires d'accidents réels et d'une mission télé-opérée. Dans un premier temps, nous avons proposé une ontologie d'analyse dysfonctionnelle appelée DAO et fondée sur l'ontologie de haut niveau UFO. DAO considère les aspects sociaux-techniques et environnementaux des SCS et intègre les différents types de fautes et de propriétés cognitives liés respectivement aux défaillances techniques et aux erreurs humaines. Le modèle conceptuel de DAO est exprimé en OntoUML et formalisé en langage OWL afin de fournir un support de raisonnement. Ensuite, un pont sémantique est établi entre les mesures de sécurité, les buts de sécurité et les exigences de sécurité par le développement d'une ontologie de gestion de sécurité orientée-but, appelée GOSMO. La gestion des décisions de sécurité s’appuie sur la réinterprétation du modèle de contrôle d'accès Or-Bac d'un point de vue sécurité-innocuité. Afin d'assurer la cohérence globale des exigences, GOSMO permet de structurer la gestion des évolutions des exigences et leur traçabilité.Safety is an emergent property of safety critical systems (SCS), including railway systems. This emergent aspect exacerbates their development process and requires a thorough reasoning to reduce hazards. This thesis proposes an ontological approach that integrates safety activities from the early design stages of SCS. This structured framework provides a semantic harmonization between the involved domains, such as safety engineering and Goal Oriented Requirements Engineering (GORE). The business logic integrated in this approach is validated by real rail accident scenarios and a remotely operated task. At first, we proposed a dysfunctional analysis ontology called DAO and based on the high-level ontology UFO. DAO considers the socio-technical and environmental aspects of SCS and integrates the different types of faults and cognitive properties that are respectively related to technical failures and human errors. The DAO conceptual model is expressed in OntoUML and formalized in OWL language in order to provide a reasoning support. Then, a semantic bridge is established between safety measures, safety goals and safety requirements through the development of a goal-oriented security management ontology, called GOSMO. The management of safety decisions is based on the reinterpretation of the Or-Bac access control model from a safety point of view. In order to ensure the overall consistency of requirements, GOSMO allows structuring the management of requirements changes and their traceabilit
From a Solution Model to a B Model for Verification of Safety Properties
No full textIn 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
Automated Risk Assessment of Shell-Based Attacks Using a LLM
No full textA honeypot is an effective tool for luring attackers and collecting information on their methods. However, honeypots are vulnerable to exploitation and can become attack vectors, necessitating enhanced security. One way to improve security is by analyzing input submitted to the honeypot and assigning a risk level to determine execution, especially important for SSH adaptive honeypots. However, in the literature, only a simple binary classification is used to classify commands as either severe or non-severe. Motivated by this gap, we propose a novel approach to assess the risk of shell commands by classifying them into five risk levels ranging from very low risk (R0) to extremely high risk (R4), evaluating the potential adversarial impact of executing them on a system. The proposed approach is then used to build a classification model using a large-language model (LLM), RoBERTa, to automatically assess commands based on their defined risk levels. We evaluate this model against two other classifiers using two different embeddings: Bag-of-Words and Word2Vec. The evaluation result shows that the LLM-based classifier outperforms the other models in accurately assessing the risk levels of shell commands
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
No full textThis volume contains papers presented at the fifth international conference on Reliability, Safety and Security of Railway Systems: Modelling, Analysis, Verification and Certification (RSSRail 2022) We are pleased to propose a mainly physical meeting during June 1–2, 2022, organized by University Gustave Eiffel in the UIC (The Worldwide Railway Organization) building in Paris. The conference is back in Paris after its first loop: The series of conferences started in Paris in 2016 and continued in 2017 in Pistoia. In 2019, the conference took place in Lille and the 2021, edition was a special issue of the journal Formal Aspects of Computing. In 2022 we were back to where we started, after a long period of pandemic, filled with expectations for a fruitful physical event fostering networking activities and an informal but fundamental sharing of knowledg
Robust Control under Uncertainty for Seaport Handling Equipments
No full textAbstractUncertainty in transport includes mainly unavailability of transportation resource, durations of maintenance activities and the infrastructure constraints. The uncertainty influences the transportation resource availability, and consequently the planned transport schedule. Developments presented in this paper are devoted to the robustness control of transportation system. A robust control strategy towards uncertainty is presented. The presented control strategy tries to reduce unavailability of machines in transportation system and to minimize the total transfer time. To illustrate the effectiveness and accuracy of proposed robustness approach, an application to a seaport handling equipments is outlined
- …
