Software safety in nuclear engineering domain has become an important issue as relay-based analog systems are being replaced by PLC-based software. Therefore several formal specification methods have been developed and successfully applied to the systems to improve their quality. In the development of KNICS APR-1400 RPS, NuSCR was used in specifying the requirements and the FBD (Function Block Diagram), a programming language for PLC, is used to realize them into design specifications.
This thesis proposes a technique for synthesizing FBD software from NuSCR formal specification. In case of KNICS APR-1400 RPS, the synthesis is possible because the NuSCR requirements were specified so rigorously and completely that they can be used to generate FBD program without further information. Our technique translates the NuSCR requirements into behaviorally equivalent FBD programs. Furthermore, the whole synthesis procedure was formally defined and its correctness was proved. This synthesis prevents design errors induced by manual FBD programming and consequently reduces the efforts required in the verification and validation.
This thesis also provides a translation technique from FBD to Verilog, which enables the use of VIS verification system and SMV model checker in the verification of the FBD. In the development of complex software system, a number of design enhancement in later are common cases and they may give rise to behavioral changes and safety critical errors. In particular, the VIS checks the behavioral equivalence between the FBDs, therefore it can be used in guaranteeing the behavioral preservation between the FBDs before and after the modification of design. Proposed techniques are being applied to KNICS APR-1400 RPS that is being developed in KNICS consortium.
원자력 공학 분야에는 기존에 널리 사용되던 RLL (Relay Ladder Logic) 기반의 아날로그 시스템이 PLC (Programmable Logic Controller) 기반의 소프트웨어로 교체됨에 따라 소프트웨어의 안전성에 대한 관심이 집중되고 있다. 정형기법은 소프트웨어의 품질과 안전성을 크게 향상시킬 수 있는 기법으로 널리 인식되고 있으며, 원자력 분야에서도 여러 정형 명세 기법들이 성공적으로 적용되고 있다. KNICS 컨소시엄에서 개발 중이며 또한, 본 연구의 적용 대상인 차세대 원자로 APR-1400 RPS 시스템은 소프트웨어 요구사항명세가 NuSCR 정형명세기법을 이용하여 더 이상의 추가적인 정보 없이 FBD 프로그램을 구현 할 수 있을 정도로 자세하고 완벽하게 작성되었다. 따라서, NuSCR 정형명세로 부터 FBD 프로그램을 기계적으로 생성하는 기법이 크게 요구되고 있다. FBD 생성기법은 수동으로 FBD 프로그램을 작성할 때 발생할 수 있는 디자인 오류들을 방지할 수 있으므로 소프트웨어 확인 및 검증에 대한 비용을 크게 줄일 수 있을 것으로 예상된다. 본 연구에서는 NuSCR 정형명세로부터 FBD 프로그램을 생성하는 기법을 제안한다.
먼저 본 연구는 소프트웨어의 요구사항이 NuSCR 정형명세 기법으로 명세되어 있음을 가정하며, 이 정형명세는 제안된 기법을 통해 동일한 행위를 보이는 FBD 프로그램으로 기계적으로 생성된다. 전체 생성과정은 모두 정형적으로 정의 및 증명되어 있으므로, 디자인 단계의 FBD 프로그램에 대한 중복되는 검증 작업을 크게 줄일 수 있는 장점이 있다. 하지만, 원자력 발전소와 같은 복잡한 시스템을 개발할 때에는, 요구사항명세가 완성된 후에도 여러 디자인 변경이 발생하는 경우가 많으며, 또한 이러한 디자인 변경은 기계적으로 생성된 FBD 프로그램의 수정을 요구하게 된다. 이러한 FBD에 대한 수정은 심각한 오류를 야기할 수 있으므로, 이에 대한 정확한 검증이 요구된다. 따라서 본 연구에서는 FBD 프로그램을 Verilog로 변환하는 변환기법을 제공함으로써 VIS와 SMV와 같은 정형도구를 사용하여 정형검증을 수행할 수 있도록 하고 있으며, 이 방법을 통하여 빈번히 발생하는 디자인 변경에 유연하게 대처할 수 있게 하고 있다. 본 연구에서 제안하고 있는 FBD 생성기법은 현재 개발중인 KNCIS APR-1400 RPS 시스템에 적용중이며, FBD 생성과 검증을 지원하는 도구도 또한 함께 개발중이다.
