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

• Autorzy: Mirabadi A. , Yazdi M.

Warianty tytułu

PL

Automatyczna generacja i sprawdzanie tablic zależności dla systemu sterowania ruchem kolejowym z wykorzystaniem metody automatów skończonych i formalnych technik weryfikacji

• Języki publikacji: EN

Abstrakty

EN

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

PL

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.

Słowa kluczowe

EN

railway traffic; railway infrastructure

PL

ruch kolejowy; infrastruktura kolejowa; metoda automatów skończonych

• Wydawca: Wydawnictwo Politechniki Śląskiej
• Czasopismo: Transport Problems
• Rocznik: 2009
• Tom: T. 4, z. 1
• Strony: 103--110
• Opis fizyczny: Bibliogr. 7 poz.

Twórcy

autor

Mirabadi A.

autor

Yazdi M.

• Iran University of Science and Technology, School of Railway Engineering (S.R.E) Iran,Tehran, Narmak,

Bibliografia

• 1. Eisner C.: Using symbolic model checking to verify the railway stations of hoornkersenboogerd and heerhugowaard. Proc. of Conf. on Correct Hardware Design and Verification Methods (CHARME’99)’, Vol. 1703 of LNCS, Springer-Verlag, 1999.
• 2. Simpson A., Woodcock J., Davies J.: The mechanical verification of solid state interlocking geographic data. Proc. of Formal Methods Pacific (FMP’97)’, Discrete Mathematics and Theoretical Computer Science Series, Springer-Verlag, 1997, p. 223-243.
• 3. Hubber M.: Towards an industrially applicable model checker for railway signalling data. Masters thesis, University of York, 2001.
• 4. Tombs D., Robinson N., Nikandros G.: Signalling control table generation and verification. Proc. of the Conference on Railway Engineering (CORW2000)’, Railway Technical Society of Australasia, November, 2002.
• 5. Office of rail regulation: Railway safety principles and guidance. Section D, guidance on signalling, April, 2006.
• 6. Cavada R., et al.: NuSMV 2.2 Tutorial. ITC-irst - Via Sommarive 18, 38055 Povo (Trento). Italy, 2006.
• 7. Emerson E.: Temporal and modal logic. Handbook of Theoretical Computer Science, Vol. b, Elsevier Science Publishers, 1990.