ABSTRACT The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction‐based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its consideration of transitions from unreachable safe states to unsafe states. Invariants that reduce the state space to an over‐approximation of reachable states, excluding transitions from safe to unsafe states, can help remove these false positives. However, such invariants are difficult to deduce automatically. In previous work, we have demonstrated that reinforcement learning (RL) and descriptive statistics can be used to generate candidate invariants, trivially within small programs, and can be realistically scaled to industrial settings using hardware‐accelerated implementations. This paper extends our hybrid approach that uses General Purpose Graphics Processing Units (GPGPUs) to overcome these challenges while scaling effortlessly horizontally and in a distributed manner. We detail the implementation of a three‐kernel pipeline responsible for consuming streamed data and computing correlation coefficients. Finally, we present a breadth of time samples that highlight the performance and scalability of this approach.

Summary Continuous evolution and improvement of GPGPUs has significantly broadened areas of application. The massively parallel platform they offer, paired with the high efficiency of performing certain operations, opens many questions on the development of suitable techniques and algorithms. In this work, we present a novel algorithm and create a massively parallel, GPGPU‐based solver for enumerating solutions of the N‐Queens problem. We discuss two implementations of our algorithm for GPGPUs and provide insights on the optimizations we applied. We also evaluate the performance of our approach and compare our work to existing literature, showing a clear reduction in computational time.

OnTrack is a tool that supports workflows for railway verification that has been implemented using model driven engineering frameworks. Starting with graphical scheme plans and finishing with automatically generated formal models set-up for verification, OnTrack allows railway engineers to interact with verification procedures through encapsulating formal methods. OnTrack is grounded on a domain specification language (DSL) capturing scheme plans and supports generation of various formal models using model transformations. In this paper, we detail the role model driven engineering takes within OnTrack and reflect on the use of model driven engineering concepts for developing domain specific formal methods toolsets.

Virtual coupling is a promising innovation aimed at increasing railway capacity. Compared to current railway signaling systems, it allows two or more trains to run with reduced headway between them. However, such reduced headways are a challenge to safety. In this work we consider this challenge by formally describing and verifying an approach to virtual coupling. We propose a general modeling method based on topological manifolds to describe the protection logic for virtual coupling train control systems. We also describe the basic train control elements in topological terms and analyze the line condition of our virtual coupling logic. We establish that the line condition safety requirements and its representation as a manifold are equivalent and further provide a formal definition of the concept of a movement authority with manifold notations. This allows us to consider the dynamic behavior of trains and a series of theorems that establish the correctness of our protection logic for virtual coupling. Finally, we apply the presented methods to a case study. The results show that the proposed method provides a suitable way to realize a virtual coupling logic safely.

In this paper, we present a novel approach to providing students with hands-on learning experiences for security testing. Specifically, we give details of a Raspberry Pi-based lab architecture which we developed as part of a security course, and provide example lab tasks that such an architecture affords. We provide evidence that introducing such hands-on labs within the security course directly improved student performance. Finally, we compare our approach to other existing approaches of which we are aware that are based on virtual machines and networks.