Some trends in formal methods applications to railway signaling

Railway signaling is often considered as one of the most fruitful areas of intervention by formal methods. This chapter offers insight into the actual industrial usage of formal methods in this field, which does not yet meet the promises of the aforementioned success stories, but is steadily increasing. The external conditions that are driving industrial choices are also discussed. The EN50128 guidelines by the European Committee for Electrotechnical Standardization (CENELEC) regarding the development of software for railway signaling are discussed. The chapter reports on a comparative case study of the applicability of different formal methods to railway signaling. It talks about the applications in the railway domain of one such formal method, namely B. The chapter focuses on formal methods applications to railway signaling equipment, which is divided into train control systems and interlocking systems.