Formal Development of a Safety Controller for Machine Learning Outputs in Vital Railway Systems

• Thierry Lecomte CLEARSY https://orcid.org/0000-0001-8977-4827

Resumo

The integration of machine learning (ML) into safety-critical railway systems raises significant challenges for certification, as current safety standards require transparent, fully specified system designs, whereas ML models are inherently opaque after training. This short paper presents an on-going work where a proof-of-concept architecture is explored, in which ML outputs are validated by an independently implemented safety controller. The controller is developed using the B method and deployed on a safety-grade computing platform, focusing on free track detection as the application scenario. In this setup, a convolutional neural network proposes a candidate track path, and the safety controller verifies its consistency with physical and geometric constraints. The work illustrates how formal specification and proof can be applied to the safety component in order to constrain the influence of ML, without addressing the full certification process. This proof-of-concept highlights the potential for combining formally developed safety logic with advanced perception modules in railway applications, while acknowledging that further work is required for industrial deployment.

Palavras-chave: formal methods, safety critical, railway