The formal verification of FBD program is required in nuclear engineering domain as traditional relay-based analog systems are being replaced with digital PLC based software. This paper proposes a way to formally verify the FBD program. For this purpose, Verilog model is automatically translated from the FBD program, then Cadence SMV performs model checking. We demonstrated the effectiveness of the suggested approach by conducting a case study of the nuclear reactor protection system, which is currently being developed in Korea.
원자력 공학 분야에서는 기존에 사용되던 RLL (Relay Ladder Logic) 기반의 아날로그 컨트롤러가 PLC (Programmable Logic Controller) 기반의 디지털 시스템으로 대체되면서 소프트웨어의 안전성에 대한 중요성이 높아지고 있다. KNICS 컨소시엄에서 개발중인 차세대 원자로 APR-1400 RPS 노심보호 시스템은 PLC 개발 언어의 하나인 FBD (Function Block Diagram)으로 SDS (Software Design Specification: 상세설계)가 작성되어 있으며, 이를 대상으로 다양한 V&V 가 이루어지고 있다. 정형기법은 소프트웨어의 안전성을 극대화 시키는 방법으로서 주목받고 있으며, 원자력 분야에서도 적용되고 있다. 이 가운데서 모델체킹 기법이 FBD로 작성된 이 시스템을 정형검증하는데 사용된다. 본 연구에서는 FBD 프로그램을 정형검증하기 위한 방법을 제안한다.
먼저 본 연구는 모델체커로 Cadance SMV를 사용하며, 모델체킹에 사용될 속성이 원자력 분야 전문가들에 의해 정해져 있음을 가정한다. 모델체킹이 행해질 대상은 FBD 프로그램으로부터 자동 변환된 Verilog 모델이 된다. Verilog 모델은 본 연구에서 제안된 변환기법에 의하여 FBD로부터 생성된다. FBD Verifier 도구가 개발되어 Verilog 모델 자동생성, 모델체커 실행, 반례 분석에 이르는 일련의 정형검증 과정을 지원한다. 제안된 방법을 KNICS APR-1400 RPS 시스템에 적용하여 다수의 오류를 발견하였다.
