부산대학교 도서관

In Railway, The interlocking is safety essential systems, and if it malfunction, they can cause major accidents, so high safety requirements must be met. In order to prevent interlock design errors and verify safety, the need for research on the introduction of formal methods has been raised, and in the case of Europe, projects for standardization are underway. This paper modeled the interlocking logic for signal, point machine, and routes configuration by applying the Petrinet model, one of the formal methods, and verified the safety of interlocking devices.