MODELLING AND FORMAL VERIFICATION ON TRAIN INTERLOCKING SYSTEM USING MODEL CHECKING METHOD

• Main Author: PRADITYO (NIM : 13313022) ; BENEDICTUS ARSTYO NUGROHO (NIM : 13313096), KEVIN
• Format: Final Project
• Language: Indonesia
• Online Access: https://digilib.itb.ac.id/gdl/view/28442
• Institution: Institut Teknologi Bandung

Railway is a ground transportation modes that falls within the category of safety critical system and requires safety integrity level (SIL) 4. One of the main requirements of a system with SIL-4 is the formal verification of software and hardware systems used to ensure the safety of system operation. The interlocking system in the operation of the railroad forms a system that governs the journey and direction of rail movement. To fulfill SIL 4 safety standards, this paper proposes a modular modeled of rail interlocking system using petri net and finite state automata (FSA). The safety specification of the operation of the interlocking system model is defined by using the logic temporal type computational tree logic (CTL). The model checking for model verification of specifications is executed on the TAPAAL and UPPAAL model checker. If the model complies the specifications, the model checker will produce a "satisfied" result and if it does not then the model checker will give a "not satisfied" result which can then be the basis for model correction. The result of verification and model refinement with formal method in this research indicates that the model checking method has the potential to be implemented in the design and verification of rail interlocking system. Models that satisfy the specifications are then implemented into the graphical user interface (GUI) in Matlab.