LEADER 09358nam 2200493 450 001 996475771203316 005 20231110225037.0 010 $a3-031-05814-3 035 $a(MiAaPQ)EBC6995047 035 $a(Au-PeEL)EBL6995047 035 $a(CKB)22444514500041 035 $a(PPN)268951829 035 $a(EXLCZ)9922444514500041 100 $a20221210d2022 uy 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 00$aReliability, safety, and security of railway systems : modelling, analysis, verification, and certification $e4th international conference, RSSRail 2022, Paris, France, June 1-2, 2022 : proceedings /$fedited by Simon Collart-Dutilleul, Anne E. Haxthausen, Thierry Lecomte 210 1$aCham, Switzerland :$cSpringer,$d[2022] 210 4$d©2022 215 $a1 online resource (245 pages) 225 1 $aLecture Notes in Computer Science ;$vv.13294 311 08$aPrint version: Collart-Dutilleul, Simon Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification Cham : Springer International Publishing AG,c2022 9783031058134 320 $aIncludes bibliographical references and index. 327 $aIntro -- 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. 327 $a5.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. 327 $aReferences -- 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. 327 $a4 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. 410 0$aLecture Notes in Computer Science 606 $aRailroads$xSafety measures 615 0$aRailroads$xSafety measures. 676 $a005.1 702 $aCollart-Dutilleul$b Simon 702 $aHaxthausen$b Anne E. 702 $aLecomte$b Thierry 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996475771203316 996 $aReliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification$92860157 997 $aUNISA