Model files for the article "A Formal Model of Train Control with AI-based Obstacle Detection".
You can view the interactive HTML traces at: https://stups.hhu-hosting.de/models/kilok/HTML_Traces/
-
Final authenticated version is available onliny at: https://link.springer.com/chapter/10.1007/978-3-031-43366-5_8
@InProceedings{10.1007/978-3-031-43366-5_8,
author="Gruteser, Jan
and Gele{\ss}us, David
and Leuschel, Michael
and Ro{\ss}bach, Jan
and Vu, Fabian",
editor="Milius, Birgit
and Collart-Dutilleul, Simon
and Lecomte, Thierry",
title="A Formal Model of Train Control with AI-Based Obstacle Detection",
booktitle="Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="128--145",
abstract="The research project KI-LOK aims to develop a certification methodology for incorporating AI components into rail vehicles. In this work, we study how to safely incorporate an AI for obstacle detection into an ATO (automatic train operation) system for shunting movements. To analyse the safety of our system we present a formal B model comprising the steering and AI perceptions subsystems as well as the shunting yard environment. Classical model checking is applied to ensure that the complete system is safe under certain assumptions. We use SimB to simulate various scenarios and estimate the likelihood of certain errors when the AI makes mistakes.",
isbn="978-3-031-43366-5"
}