  Formal methods are mathematically-based techniques for the rigorous
development of software-intensive systems. The railway signaling domain is a
field in which formal methods have traditionally been applied, with several
success stories. This article reports on a mapping study that surveys the
landscape of research on applications of formal methods to the development of
railway systems. Our main results are as follows: (i) we identify a total of
328 primary studies relevant to our scope published between 1989 and 2020, of
which 44% published during the last 5 years and 24% involving industry; (ii)
the majority of studies are evaluated through Examples (41%) and Experience
Reports (38%), while full-fledged Case Studies are limited (1.5%); (iii) Model
checking is the most commonly adopted technique (47%), followed by simulation
(27%) and theorem proving (19.5%); (iv) the dominant languages are UML (18%)
and B (15%), while frequently used tools are ProB (9%), NuSMV (8%) and UPPAAL
(7%); however, a diverse landscape of languages and tools is employed;
  (v) the majority of systems are interlocking products (40%), followed by
models of high-level control logic (27%);
  (vi) most of the studies focus on the Architecture (66%) and Detailed Design
(45%) development phases. Based on these findings, we highlight current
research gaps and expected actions. In particular, the need to focus on more
empirically sound research methods, such as Case Studies and Controlled
Experiments, and to lower the degree of abstraction, by applying formal methods
and tools to development phases that are closer to software development. Our
study contributes with an empirically based perspective on the future of
research and practice in formal methods applications for railways.
