Formalizing for Proving the System Safety of the Software Component for a Small Sized Guided Transport System

This paper focuses on the design and analysis of a safe software component respecting the signalling system of railway applications, specifically addressing the challenges related to ensuring safe train movements. The proposed system incorporates hybrid aspects, combining discrete and continuous behaviours, to effectively manage train operations. The Rodin platform and the Why3 prover are considered to provide formal verification and validation of the system’s correctness. The approach refers to existing norms, like subset 125 and industrial feed backs for formal proofs of safety properties in the metro area. Nevertheless, as the considered 8 vehicles seats autonomous guided systems running on tires, the dynamic this less than two tones cyber physical system could be quite different. As a consequence, holding the exact equation must be performed to check the consistency of common assumptions. The Why3 prover is integrated into the development process, allowing for the verification of system properties and the generation of proof obligations. This enhances the assurance of the system’s correctness and compliance with safety requirements. The combination of the Rodin platform, which supports the formal modeling and analysis of hybrid systems, and the Why3 prover, which provides powerful reasoning capabilities, offers a comprehensive approach to the design and verification of complex signalling systems in railway applications. The proposed methodology contributes aims to insure safety by comparing industrial approach consistency with industrial feed-backs and norms.