Automatic generation and verification of railway interlocking control tables using FSM and NuSMV

Due to their important role in providing safe conditions for train movements, railway interlocking systems are considered as safety critical systems. The reliability, safety and integrity of these systems, relies on reliability and integrity of all stages in their lifecycle including the design, verification, manufacture, test, operation and maintenance. In this paper, the Automatic generation and verification of interlocking control tables, as one of the most important stages in the interlocking design process has been focused on, by the safety critical research group in the School of Railway Engineering, SRE. Three different subsystems including a graphical signalling layout planner, a Control table generator and a Control table verifier, have been introduced. Using NuSMV model checker, the control table verifier analyses the contents of control table besides the safe train movement conditions and checks for any conflicting settings in the table. This includes settings for conflicting routes, signals, points and also settings for route isolation and single and multiple overlap situations. The latest two settings, as route isolation and multiple overlap situations are from new outcomes of the work comparing to works represented on the subject recently

---

Ze względu na konieczność zapewnienia bezpiecznych warunków dla ruchu pociągów, systemy sterowania ruchem kolejowym muszą być rozpatrywane jako systemy bezpieczeństwa krytycznego. Niezawodność i bezpieczeństwo tych systemów opiera się na niezawodności i integralności wszystkich etapów cyklu ich powstawania, zawierającego projektowanie, weryfikację, produkcję, testowanie, pracę i utrzymanie. W artykule została przedstawiona automatyczna generacja i weryfikacja tablic zależności jako jeden z najważniejszych etapów w procesie projektowania urządzeń SRK, opracowana przez grupę badawczą ze Szkoły Inżynierii Kolejowej, SRE. Wprowadzono trzy różne podsystemy: planowanie układu sygnalizacji, generator i weryfikator tablic. Używając technik formalnych, weryfikator tablic analizuje ich zawartość (bezpieczne warunków ruchu pociągu) i sprawdza przebiegi kolizyjne. Obejmuje to ustawienia sprzecznych tras, jak również punktów dla pojedynczych i wielokrotnych sytuacji zachodzenia przebiegów.