RESEARCH DIRECTIONS REGARDING THE ADOPTION OF FORMAL METHODS IN THE RAILWAY SIGNALING SECTOR: DETERMINANTS AND NEXT STEPS FOR FUTURE-PROOF RAILWAYS

Abstract

The terms Formal Methods (FMs) refer to a set of techniques and software toolkits that, based on mathematical rigor, can enhance safety, security, and the efficient operation of a wide range of systems. Considering that several innovative FMs applications have been performed over the last few decades, the utility of toolkits that are based on FMs has already been showcased in several industrial settings, such as the avionics and automotive industries, medical devices, computer software, and hardware systems, and finally, the railways and the railway-signalling sector. The current article focuses on the last of the aforementioned sectors, that of railway signalling, and aims to analyse research directions that regard the adoption of FMs in signalling. Despite the benefits and the availability of reports on the topic, the implementation of the adoption of FMs can be considered yet to be successful in most organizations that develop related systems. The authors have observed that this implementation lag in the adoption of FMs may stem from the absence of systematic approaches to the study of adoption. In that regard, a set of five Research Questions (RQs) is introduced in this article for the adoption of FMs in railway signalling systems. Furthermore, answers regarding two of those questions are given within the current article regarding: (i) studies on the adoption of FMs, and (ii) successful applications and benefits of FMs. The remaining three RQs are intended to point out issues for future research. By providing answers to all five RQs, it is expected that a map for the demand of FMs applications in railway signalling is introduced in the following years, as well as the role of the potential stakeholders in those applications.