A Study on the Safety Verification of Interlocking Systems Using Event-B Methods

철도 시스템은 수많은 열차와 선로가 복잡하게 연결된 시스템으로, 효율적이면서도 안전한 운영이 필수 불가결한 요소이다. 이러한 안전성을 보장하는 핵심 장치 중 하나가 바로 연동장치(Interlocking System)이며, 신호기(Signal)와 선로전환기(Point Switch Machine)의 상태를 실시간으로 제어하고 열차 간 충돌 및 추돌을 방지하는 중요한 장치로서 철도 운행의 신뢰성을 높이는 역할을 수행한다. 현대의 철도 신호시스템의 복잡성 증가와 함께 신호시스템의 오류는 치명적인 사고로 이어질 수 있기 때문에 시스템의 안전성과 신뢰성을 보장하는 것이 매우 중요하며, 시스템의 안전성을 엄격하게 검증하는 것이 필수적이다. 기존의 테스트 기반 방법론은 시스템의 일부만을 검증하는 데 한계가 있기 때문에 Event-B와 같은 형식적 방법론을 적용하여 시스템의 모든 상태와 동작을 수학적으로 검증하는 것이 필요하다.