This keynote presents CLEARSY's journey from safetycritical railway automation to broader applications in autonomous mobility. Drawing from global deployments of automatic train systems, we show how railways function as large-scale robotic systems with embedded autonomy, localization, and fail-safe mechanisms. We then explore CLEARSY's innovations in ground, aerial, and underwater autonomy, highlighting shared challenges in navigation, sensor fusion, and environment interaction. The role of advanced sensors, robust hardware, and formal modeling is emphasized across all domains. A core theme is the integration of safety, verification, and validation into robotics designrooted in CLEARSY's railway experience. The talk also addresses the transition from deterministic systems to complex, uncertain environments, proposing cross-domain methodologies for trustworthy autonomy. By bridging industry and research, CLEARSY supports the development of safe, deployable autonomous technologies. This keynote invites collaboration to ensure that the next generation of robotic systems is as safe as it is intelligent.

This extended abstract reports on recent industrial activities exploring pragmatic and controlled uses of AI in railway systems developed with formal methods. First, large language models are used to synthesize and query large-scale railway technical specifications, improving accessibility while requiring systematic human validation. Second, early experiments assess AI-assisted generation of interactive proof scripts for B method proof obligations, showing initial productivity gains but substantial research challenges. Third, AI-based perception is integrated into railway safety functions, where machine learning acts solely as a proposer whose outputs are redundantly checked by a formally verified safety controller. Finally, a proof of concept applies multimodal language models to relay-based railway interlocking systems, automatically transforming relay diagrams into propositional logic specifications applicable to new diagrams. The results confirm that AI-assisted formalization is feasible and accessible, opening promising perspectives for advancing automation and trustworthiness in railway formal verification.

The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this article, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.

This keynote presents CLEARSY’s journey from safety-critical railway automation to broader applications in autonomous mobility. Drawing from global deployments of automatic train systems, we show how railways function as large-scale robotic systems with embedded autonomy, localization, and fail-safe mechanisms. We then explore CLEARSY’s innovations in ground, aerial, and underwater autonomy, highlighting shared challenges in navigation, sensor fusion, and environment interaction. The role of advanced sensors, robust hardware, and formal modeling is emphasized across all domains. A core theme is the integration of safety, verification, and validation into robotics design—rooted in CLEARSY’s railway experience. The talk also addresses the transition from deterministic systems to complex, uncertain environments, proposing cross-domain methodologies for trustworthy autonomy. By bridging industry and research, CLEARSY supports the development of safe, deployable autonomous technologies. This keynote invites collaboration to ensure that the next generation of robotic systems is as safe as it is intelligent.

Atelier B has played a crucial role in ensuring the safety of critical systems for more than three decades. This presentation explores the recent evolution of Atelier B, from the last keynote in 2016 in Linz to its current, expanded role in system engineering across industries. We will revisit key milestones, such as the modeling of complex systems, the development and programming of the CLEARSY Safety Platform, and its use in educating students and engineers. The session will also showcase how the versatility of Atelier B has been harnessed to model, prove, and implement robust systems - from automated metros to industrial control. Through these advancements, Atelier B continues to shape the landscape of high-integrity software development, merging mathematical rigor with practical, real-world applications.

Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

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.

ERTMS aims to facilitate train traffic in Europe by providing a single, interoperable framework. ERTMS represents a set of several thousand pages of specification, covering both high-level and (very) low-level aspects. Since its creation in the 1990 s, it has evolved regularly, with baseline 4 being published in 2023. However, it is proving rather difficult to implement and deploy. It has little feedback compared with the history of the railway world in general, particularly for the highest levels of supervision. The specification, expressed in the form of thematic SUBSETS, give direction but leave a great deal of freedom to manufacturers. The verification work being carried out today relates to the compliance of on-board and trackside equipment with the SUBSETS of the standard, mainly by means of simulation and test benches. This article presents some of the formal verification and validation methods, including formal modelling, automatic proof and model-checking, that are being used today to improve the confidence level of actual deployments.

Although Formal Methods have been used for decades in the development of industrial critical systems, there are still many products that do not use this technology. The use of Formal Methods in such a context is generally highly recommended, but not mandatory, as other technologies may be used as support to certify the safety of the systems. Relay-based railway interlocking systems, for instance, are legacy systems used in the majority of railway installations and whose safety has been attested through their use for decades. Their maintenance, however, requires analysis to avoid losing their safety features. In previous papers, we have presented the CLEARSY Safety Platform (CSSP) and how it can be used to analyse and replace these legacy interlocking systems in a safety-proved manner using certified industrial tools. In this paper, we extend this discussion to present how the CSSP can be used to monitor the legacy relay-based RIS to improve their safety during their execution. The strategy is to describe the system safety properties using logic and then implement it in the CSSP, which in turn is responsible for monitoring the system components to ensure its correct functioning and raise flags when an unsafe state is found. The benefits of using our approach in industry are discussed as we present how it can be applied in two industrial case studies.

In previous work, we have presented a methodology for the specification and verification of relay-based Railway Interlocking Systems (RIS) based on their transient states. By using CSP as formal support, it is possible to use a model checker in order to analyse the safety of such critical systems as a way to improve their safety. However, this type of verification tends to consume a lot of computational resources, which hinders the use of this methodology for industrial systems. This work presents a proposal for a new methodology for the specification of RIS. In this work we rebuild the whole model by changing the notion of components, integrating them in the core of the model while keeping their interface visible to the end-user. In this context, it is possible to maintain the concepts of instantiating and combining components at the same time we reduce the number of components and states as a way to alleviate the time spent on model checking. Besides, we propose a new methodology of verification based on the decomposition of the model. Our new proposed approach supports the analysis of a bigger set of properties of these systems, like the analysis of the Ringbell Effect, short circuits, deadlocks, divergences, and components that cannot be activated at the same time. In order to evaluate our approach, a new industrial case study is modelled and analysed.

Securing a safety-critical system is a challenging task, because safety requirements have to be considered alongside security controls. We report on our experience to develop a security architecture for railway signalling systems starting from the bare ...

System safety is based on the implementation of technical and organisational principles to ensure that a feared event cannot occur more frequently than expected. Such a demonstration, so-called safety case, relies on domain specific standards which capitalise on experience gained after decades of development and operation. For more than a decade, the threat of human attacks aimed at disrupting the operation of such systems has become more acute. In the railways, communications between on board and track-side equipment are naturally subject to targeted attacks aimed at reducing the availability of the equipment or disrupting its operational safety to the point of creating accidents. This paper aims to sketch the range of logical and hardware attacks practised today that could be used in the future to attack railway systems to make them less available or less secure. It also presents a combination of techniques and technologies that, assisted by formal methods, can reduce the chances of success of such attacks.

Despite significant advancements in the design of formal integrated development environments, applying formal methods in software industry is still perceived as a difficult task. To ease the task, providing tools that help during the development cycle is essential but proper education of computer scientists and software engineers is also an important challenge to take up. This paper summarises our experience of 20 years spent in the education of engineers, either colleagues or customers, and students, together with the parallel design and improvement of supporting modelling tools.

The distribution of safety functions along the tracks requires the networking of the ECUs (Electronic Control Unit is an embedded system that controls one or more electrical systems or subsystems) that support them, to facilitate their operation and maintenance. The latter enables logs to be sent, commands to be received and sent that will lead to a state change of one of the connected equipment, and the ECU application software to be updated. All these activities are naturally subject to targeted attacks aimed at reducing the availability of the equipment or disrupting its operational safety to the point of creating accidents. This article presents an innovative approach partitioning security and safety on two different computers. One computer connected to the network ensures security and is regularly updated according to known threats. The other computer ensures safety and communicates only through a secure filter. Each computer embeds technological elements that have been specified, implemented and proven with 2 different formal methods.

In this paper, we review software-based technologies already known to be, or expected to become essential for autonomous train control systems with grade of automation GoA 4 (unattended train operation) in existing open railway environments. It is discussed which types of technology can be developed and certified already today on the basis of existing railway standards. Other essential technologies, however, require modifications or extensions of existing standards, in order to provide a certification basis for introducing these technologies into non-experimental “real-world” rail operation. Regarding these, we check the novel pre-standard ANSI/UL 4600 with respect to suitability as a certification basis for safety-critical autonomous train control functions based on methods from artificial intelligence. As a thought experiment, we propose a novel autonomous train controller design and perform an evaluation according to ANSI/UL 4600. This results in the insight that autonomous freight trains and metro trains using this design could be evaluated and certified on the basis of ANSI/UL 4600 .

The railways have a quite long modelling history, covering many technical aspects from infrastructure to rolling stock, train movement, maintenance, etc. These models are mostly separate and operated independently by various stakeholders and with diverse objectives. This article presents some of the various digital modelling activities, including formal ones, that are undertaken by the railway industry, for design, development, validation, qualification, and exploitation. It also introduces trends toward regrouping models to obtain more significant results together with a larger scope, prefiguring digital twins.

The CLEARSY Safety Platform (CSSP) is both a hardware and software platform aimed at developing safety critical applications. A smart combination of hardware features (double processor) and formal method (B method and code generators) was used to produce a SIL4-ready platform where safety principles are built-in. A first version, SK0, was released for education purpose with a restricted application template. An industry-strength version, CS0, was then released, providing more degrees of freedom at the cost of a more tricky development and engineering process. This article presents the new CS0 modelling paradigm, lists the conditions to be verified by the system developed, and briefly introduces a first application, software only: a safety flasher.

The CLEARSY Safety Platform (CSSP) was designed to ease the development of safety critical systems and to reduce the overall costs (development, deployment, and certification) under the pressure of the worldwide market. A smart combination of hardware features (double processor) and formal method (B method and code generators) was used to produce a SIL4-ready platform where safety principles are built-in and cannot be altered by the developer. Summarizing a 5-year return of experience in the effective application in the railways, this article explains how this approach is a game-changer and tries to anticipate the future of this platform for safety critical systems. In particular, the education of future engineers and the seamless integration in existing engineering processes with the support of Domain Specific Languages are key topics for a successful deployment in other domains. DSL like Robosim to program mobile robots and relay circuits to design railway signalling systems are connected to the platform.

Industrial applications involving formal methods are still exceptions to the general rule. Lack of understanding, employees without proper education, difficulty to integrate existing development cycles, no explicit requirement from the market, etc. are explanations often heard for not being more formal. This article reports some experience about a game changer that is going to seamlessly integrate formal methods into safety critical systems engineering.