Preliminary communication
Automatic generation and verification of railway interlocking control tables using FSM and NuSMV
Ahmad Mirabadi
; School of Railway Engineering, Iran University of Science and Technology, Tehran, IRAN
Mohammad Bemani Yazdi
; School of Railway Engineering, Iran University of Science and Technology, Tehran, IRAN
Abstract
Due to the 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. 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 analyzes 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.
Keywords
railway signalling; interlocking; safety critical systems; formal methods; model checking; NuSMV
Hrčak ID:
185925
URI
Publication date:
27.11.2009.
Visits: 803 *