NSE C20- Formal Modelling of Security in Safety Critical Systems

Researchers: Ehsan Poorhadi (PhD student), Elena Troubitsyna (Assoc. Prof.), György Dán (Project manager)

Source of Funding: Trafikverket (Swedish Transport Administration)/ S2R

The project contributes to the work on security analysis of railway signalling and control systems within
Shift2Rail, and is performed as linked third party through Trafikverket. In the project the focus is on extending formal verification of safety critical networked systems, with a focus on applications in railways, e.g., including interlocking and ETCS, so that the impact of potential vulnerabilities of IT components and subsystems can be included in the safety analysis. The main challenge lies in developing a scalable yet useful abstraction for security vulnerabilities, which allows modelling and analysis in well-established frameworks based on set theory, first order logic and temporal logic.