Reliability, safety, and security of railway systems : modelling, analysis, verification, and certification : 4th international conference, RSSRail 2022, Paris, France, June 1-2, 2022 : proceedings / / edited by Simon Collart-Dutilleul, Anne E. Haxthausen, Thierry Lecomte

• Pubblicazione: Cham, Switzerland : , : Springer, , [2022]; ©2022
• Descrizione fisica: 1 online resource (245 pages)
• Disciplina: 005.1
• Soggetto topico: Railroads - Safety measures
• Persona (resp. second.): Collart-DutilleulSimon; HaxthausenAnne E.; LecomteThierry
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Intro -- Preface -- Organization -- Abstracts of Keynotes -- New Methods for Safety Demonstration in the Frame of Railway System -- Satellite-Based Train Localization for Safety Critical Applications. The Challenges of Performance Demo and Certification -- Contents -- Safe Interlocking -- Compositional Verification of Railway Interlockings: Comparison of Two Methods -- 1 Introduction -- 2 Background -- 3 Formal Verification by Model Checking -- 3.1 The RobustRailS Method -- 3.2 The Louvain Method -- 4 Compositional Verification -- 4.1 The RobustRailS Compositional Method -- 4.2 The Louvain Compositional Method -- 5 Comparison of the Two Methods -- 6 Case Study: La Louvière-Sud -- 6.1 Decomposition of LVR7 - Piéton station -- 6.2 Verification Results Using the RobustRailS Method -- 6.3 Verification Results Using the Louvain Method -- 6.4 Discussion -- 7 Related Work -- 8 Conclusions -- References -- Safety Invariant Verification that Meets Engineers' Expectations -- 1 Introduction -- 2 Reporting Safety Invariant Violations -- 2.1 Establishing System Correctness -- 2.2 The Running Example -- 2.3 Symbolic Verification of Signalling Safety Principles -- 2.4 The Running Example, Continued -- 3 Positive Demonstration of the Absence of Violations -- 3.1 Synthesising a Focused Safety Invariant -- 3.2 Computing Potential Errors -- 4 Discussion and Conclusions -- References -- Innovation in Traffic Management -- Formalization and Processing of Data Requirements for the Development of Next Generation Railway Traffic Management Systems -- 1 Introduction -- 2 OPTIMA Project -- 3 Railway System Modelling: State of Play -- 3.1 Shared Models -- 3.2 Platform-Specific Model: X2Rail-4 -- 4 OPTIMA: From Requirements to Model -- 4.1 Challenges of Model Evolution -- 4.2 Previous Works -- 5 Formalizing Data Requirements -- 5.1 Minimal Requirements... for Requirements. ; 5.2 Supporting Grammar -- 5.3 Semantics -- 5.4 Authorities -- 6 Transformation and Integration -- 6.1 Pre-processing -- 6.2 Processing and Post-processing -- 7 Conclusions and Further Works -- References -- Acceleration Techniques for Symbolic Simulation of Railway Timetables -- 1 Introduction -- 2 Symbolic Simulation -- 2.1 Primary Delays -- 2.2 Scenarios -- 2.3 Algorithm -- 3 Reduction -- 3.1 Transformation Rules -- 3.2 Iterative Approach -- 3.3 Bounded Model Checking Approach -- 4 Experimental Evaluation -- 5 Conclusion -- References -- Optimal Railway Routingpg Using Virtual Subsections -- 1 Introduction -- 2 Railway Routing in ETCS Level 3 -- 3 Motivation: The Problem of Discretization -- 4 Proposed Solution -- 4.1 Main Approach Based on A* Search -- 4.2 Resolving Collisions with VSS -- 5 Experiments -- 6 Conclusion -- References -- Safety and New Technologies -- Verification of Multiple Models of a Safety-Critical Motor Controller in Railway Systems -- 1 Introduction -- 2 Use-Case: Motor Controller -- 3 Formal Specification in Uppaal -- 4 Parameterisation and Verification with Uppex -- 4.1 Annotating Uppaal Models -- 4.2 Verifying Multiple Configurations -- 5 Lessons Learned and Future Work -- 6 Conclusions -- References -- Learning to Learn HVAC Failures: Layering ML Experiments in the Absence of Ground Truth -- 1 Introduction -- 1.1 Scientific Approach with Practical Applications -- 2 Learning HVAC Failures from Temperature Readings -- 2.1 Data Preparation -- 2.2 Machine Learning Experiment -- 2.3 Study on Rolling Stock of NS -- 3 Learning HVAC Failures from Diagnose Codes -- 3.1 Data Preparation -- 3.2 Machine Learning Experiment -- 3.3 Study on Rolling Stock of NS -- 4 Final Discussion and Perspectives -- 4.1 Temperature Readings to Detect HVAC Failures -- 4.2 Diagnose Codes to Detect and Predict HVAC Failures -- 4.3 Perspectives. ; References -- Safety -- Enhancing Autonomous Train Safety Through A Priori-Map Based Perception -- 1 Introduction -- 2 State of the Art -- 2.1 Infrastructure Modelling -- 2.2 Perception and Segmentation -- 3 Methodology -- 3.1 Our Database -- 3.2 Our Approach -- 4 Results and Analysis -- 5 Conclusion -- References -- Assigning Safe Executed Systems to Meanings -- 1 Introduction -- 2 CLEARSY Safety Platform -- 3 CSPLib -- 3.1 Timing Support -- 3.2 Proof of Timing Properties -- 3.3 Lifting Simplifying Hypotheses -- 4 Proving Reality -- 4.1 Guidelines -- 4.2 A Simple Example: Safety Flasher -- 4.3 Full Example: Train Location and Kinematics -- 5 Conclusion -- References -- Generating and Verifying Configuration Data with OVADO -- 1 Introduction -- 2 OVADO Basic Use -- 3 OVADO Use to Check Railway Systems -- 4 A New Use of OVADO to Generate Data -- 5 Adaptation of the SIL4 Process -- 6 Conclusion -- References -- The 4SECURail Formal Methods Demonstrator -- 1 Introduction -- 2 The 4SECURail Case Study -- 3 The Requirements Analysis Process -- 3.1 Semi-formal Designs -- 3.2 Executable UML Designs -- 3.3 Formal Modelling -- 3.4 Revised Natural Language Requirements -- 4 Related Works -- 5 Conclusions -- References -- ATO -- Formal Design and Validation of an Automatic Train Operation Control System -- 1 Introduction -- 2 The ATO Control System -- 3 Challenges -- 4 Formal Design of ATO -- 4.1 Requirements and Architecture -- 4.2 Development Process -- 4.3 Verification and Validation -- 5 Lessons Learned -- 6 Conclusions and Future Work -- References -- Investigating Human Error Within GoA-2 Metro Lines -- 1 Introduction -- 1.1 Context of the Problem -- 2 Analysis -- 2.1 Real-World Examples of Problems -- 2.2 Current Real-World Solutions -- 3 Synthesis -- 3.1 Solutions Within the Expansion of GoA-2 -- 3.2 Upgrading to GoA-3 -- 3.3 Decrease of Automation. ; 4 Conclusion -- References -- A Vision of Intelligent Train Control -- 1 Introduction -- 2 Background on Modern Train Control Systems -- 2.1 Basic Definitions About Connected and Autonomous Trains -- 2.2 The ERTMS/ETCS Railway Standard Specification -- 2.3 Segregated and Open Railway Environments -- 2.4 Automatic Train Operation over ETCS -- 2.5 Train Virtual Coupling -- 2.6 Certification Challenges for Autonomous Trains -- 3 Intelligent Train Control -- 3.1 Intelligent Train Operation and Protection -- 3.2 Grades of Intelligence in Train Control -- 4 Technology Enablers for Intelligent Train Control -- 4.1 Autonomic Computing and Digital Twins in Railways -- 4.2 Anomaly and Obstacle Detection, and Signal Recognition -- 4.3 Trustworthy and Explainable AI -- 5 Conclusions -- References -- Safe and Secured Telecom for Railway -- Analysis of Safety-Critical Communication Protocols for On-Premise SIL4 Cloud in Railways -- 1 Introduction -- 1.1 Motivation -- 1.2 Purpose of Paper -- 2 SIL4 Communication Requirements -- 2.1 Safe Computing Platform -- 2.2 Requirements -- 3 Railway-Specific Safety-Critical Protocols -- 4 Potential SIL4 Communication Protocols -- 4.1 OPC UA -- 4.2 DDS -- 5 Safe Communication Architecture for Railway Systems -- 6 Evaluation -- 7 Conclusion -- References -- TASC: Transparent, Agnostic, Secure Channel for CBTC Under Failure or Cyberattack -- 1 Introduction -- 2 Related Work -- 3 Overview of CBTC and Attack/Failure Model -- 3.1 Train-to-Wayside Radio Network -- 3.2 Attack and Failure Model -- 3.3 Alternative Networks for CBTC Signaling -- 4 Transparent, Agnostic, Secure Channel (TASC) System -- 4.1 Resilience Against Jamming/Interference -- 4.2 Resilience Against AP Failure -- 5 Security Discussion of TASC -- 6 Prototype for Concept Validation -- 7 Conclusion -- References -- Author Index.
• Titolo autorizzato: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
• ISBN: 3-031-05814-3
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910574052503321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture Notes in Computer Science