서지주요정보
Verification of function block diagram through verilog translation = Verilog 변환을 이용한 FBD의 정형검증
서명 / 저자 Verification of function block diagram through verilog translation = Verilog 변환을 이용한 FBD의 정형검증 / Seung-Jae Jeon.
저자명 Jeon, Seung-Jae ; 전승재
발행사항 [대전 : 한국과학기술원, 2007].
Online Access 원문보기 원문인쇄

소장정보

등록번호

8018454

소장위치/청구기호

학술문화관(문화관) 보존서고

MCS 07036

SMS전송

도서상태

이용가능

대출가능

반납예정일

초록정보

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 시스템에 적용하여 다수의 오류를 발견하였다.

서지기타정보

서지기타정보
청구기호 {MCS 07036
형태사항 v, 26 p. : 삽도 ; 26 cm
언어 영어
일반주기 저자명의 한글표기 : 전승재
지도교수의 영문표기 : Sung-Deok Cha
지도교수의 한글표기 : 차성덕
학위논문 학위논문(석사) - 한국과학기술원 : 전산학전공,
서지주기 Reference : p. 25-26
주제 Function Block Diagram
verification
model checking
Verilog translation
FBD
검증
모델체킹
Verilog 변환
QR CODE qr code