Verification of Behavioral Consistency between FBD and C programs using HW-CBMC = HW-CBMC를 이용한 FBD 프로그램과 C 프로그램의 행위 일치성 검증

다국어 초록 (Multilingual Abstract)

Controllers in safety-critical systems such as nuclear power plants often use FBD (Function Block Diagram) to design embedded software. Implementation programs of the design are implemented in programming languages such as C language. Behavior of the two programs, written in FBD and ANSI-C language, must be consistent, and it should be verified precisely.
This thesis proposes a verification technique for verifying behavioral con-sistency between FBD and C programs using HW-CBMC (Hardware-C Bounded Model Checking). The two programs which is developed using pSET are the target domain. The pSET (POSAFE-Q Software Engineering Tool), which is a loader software to program POSAFE-Q PLC and is developed as a part of the KNICS (Korea Nuclear Instrumentation & Control System) project, uses FBD to design the PLC program and generates ANSI-C program automatically. The automatically generated C program is loaded on PLC after a compiler compiles the C program.
This thesis also provides a translation technique from FBD to Verilog, which enables the use as an input program of HW-CBMC. Once the FBD program is translated into a semantically equivalent Verilog program and verification of be-havioral consistency is per-formed using HW-CBMC. This proposal makes the user can verify the behavioral consistency between FBD and C programs with-out specific knowledge about formal verification or HW-CBMC. Demonstration as a case study about the effectiveness of this proposal used one of RPS (Reactor Protection System) modules of APR-1400 (Advanced Power Reactor) in KNICS project.

국문 초록 (Abstract)

원자력 발전소나 철도, 비행기 등과 같은 안전필수시스템은 FBD와 같은 언어를 사용하여 해당 시스템에서 사용하는 PLC (Programmable Logic Controller) 프로그램을 설계한다. 설계된 FBD는 자동변환 프로그램을 이용해 ANSI-C와 같은 프로그래밍 언어로 구현되고, 구현된 프로그램은 해당 PLC의 기계어로 컴파일 되어 사용된다. 이 때, 설계된 FBD프로그램과 구현된 ANSI-C 프로그램간의 행위가 일치됨을 보장하거나 명확히 검증되어야만 안전하게 사용할 수 있다.
본 논문에서는 FBD로 설계한 프로그램과 ANSI-C 언어로 구현된 프로그램간의 행위 일치성을 검증하기 위하여 정형검증도구인 HW-CBMC를 이용한 검증 기법을 제안한다. 본 논문에서는 KNICS (Korea Nuclear Instrumentation & Control System) project에서 개발한 pSET (POSAFE-Q Software Engineering Tool) 도구를 이용해 설계한 FBD프로그램과 해당 도구 내에 포함된 Code-Generator를 이용해 변환된 ANSI-C 프로그램간의 행위 일치성 검증을 범위로 정했다.
또한, 본 논문은 HW-CBMC를 이용한 위 기법을 적용 가능하게 하기 위하여 FBD를 동일한 의미를 가지는 Verilog로 변환하는 기법과 사용자가 쉽게 검증을 수행할 수 있도록 하는 C 프로그램의 틀을 제공한다. FBD를 Verilog로 변환하기 위하여 FBD의 정형 모델을 정의하고 Verilog로 변환하기 위한 규칙을 정의하였다. HW-CBMC를 이용해 프로그램을 검증할 때, 검증 속성을 C 프로그램 내부에 삽입해야 하는데, 이러한 절차를 거치지 않도록 할 수 있는 틀을 제공한다. 본 논문에서 제안한 검증 기법이 유용함을 확인하기 위하여 KNICS 프로젝트 중 ARP-1400 (Ad-vanced Power Reactor) BP모델의 일부 모듈을 사용해 검증을 수행한 결과를 기술하였다.

목차 (Table of Contents)

• Chapter 1. Introduction = 1
• Chapter 2. Backgrounds = 4
• 2.1 pSET = 4
• 2.2 FBD = 5
• 2.3 Verilog = 6
• 2.4 HW-CBMC = 6
• Chapter 3. Translation from FBD into Verilog = 8
• 3.1 Formal Definition of FBD = 8
• 3.2 Well-formed FBD = 10
• 3.3 Translation Rules = 11
• Chapter 4. Verification of Behavioral Consistency = 15
• 4.1 Verification Process = 15
• 4.2 Template for Verification = 17
• Chapter 5. Case Study = 22
• 5.1 Target program: FIX_RISING module = 22
• 5.2 Verification Process = 24
• 5.3 Verification Results = 25
• Chapter 6. Related Work = 28
• 6.1 Equivalence Checking = 28
• 6.2 Verification of Compilers Code-Generators, or Translators = 28
• Chapter 7. Conclusion and Future Work = 30
• References = 31
• Appendix A = 35
• Appendix B = 41
• Abstract (in Korean) = 44