Event-B Methods를 이용한 연동장치 안전성 검증 연구

The railway system is a complex, with numerous trains and tracks, and efficient and safe operation is essential. One of the key devices that ensures this safety is the interlocking system, which is an important device that controls the status of signals and point switch machines in real time and prevents front collisions and rear-end collisions between trains, thereby increasing the reliability of railway operation. As the complexity of modern railway signaling systems increases, errors in the signaling system can lead to fatal accidents, so it is very important to ensure the safety and reliability of the system; it is essential to strictly verify the safety of the system. Since existing test-based methodology has limitations in verifying only parts of the system, it is necessary to apply a formal methodology such as Event-B to mathematically verify all states and operations of the system.