Railway signaling systems have experienced a certain reluctancy in evolving from mechanical and electro-mechanical systems to computer-based ones, if compared with other domains (e.g. avionics or automotive). However Formal Methods, in the broader sense of the term, have played an important role in the evolution of railway signalling industry in the last 25 years or more.
The high confidence that has been gradually achieved on the safe working of computer-based signaling system, thanks to the advances of software engineering techniques pushed by formal specification and verification techniques, is going to open new application scenarios exploiting increasingly complex systems, in which reliance on proper functioning of computer systems is even more vital.
This talk will discuss the challenges that are still posed to industry by the most modern signaling systems to verification techniques (such as the case of model-checking large interlocking systems), as well as the new challenges that innovative systems and operation scenarios are going to create.

Alessandro Fantechi is full professor at the Faculty of Engineering of the University of Florence, where he teaches at the Computer Engineering curricula, and where he has been from 2007 to to 2014 coordinator of the Computer Engineering curricula. Prof. Fantechi is an active researcher in the areas of formal description techniques, temporal logics, formal verification, and their applications to the development of safety-critical systems, with a particular experience on railway signalling systems, thanks to contacts and collaborations with main railway signalling producers. His current research is focused on the application of model-checking based formal verification methods to safety-critical systems,  and on formal aspects of software product lines. He has written over one hundred papers for international journals and conferences. From 2008 to 2011 he has been coordinator of  the ERCIM FMICS working Group. In 2016 he has been VELUX visiting professor at the University of Lyngby.