Safety assessment of dependable software system using test cases

윤상현 건국대학교 대학원 2012 국내석사

소프트웨어의 안전성은 신뢰성 있는 소프트웨어 시스템의 중요한 원리이다. 안전성 전문가들은 안전성 분석 기법들을 사용하여 안전성 요구사항들을 분석 및 보완하고 안전성 측정을 통해 분석된 안전성 요구사항들이 얼마나 반영되어있는지를 판단한다. 규제 기관들의 운영허가를 받기 위해서는 안전성 분석과 안전성 측정들을 수행해야 하지만 해당 기법들은 수행하기 어렵과 시간과 비용이 많이 드는 문제점이 있다. 본 논문에서는 테스트 케이스를 이용하여 우회적으로 안전성을 측정함으로써 안전성 측정에 소요되는 시간과 비용을 줄이는 방법을 제안한다. 우리는 안전성 속성들을 소프트웨어 고장수목의 최소절단집합에서 선출하고 테스트 케이스가 해당 안전성 속성들을 얼마나 포함하고 있는지를 정형 기법을 통해 분석하였다. 테스트 케이스가 안전성 속성들을 포함하고 있고 그 테스트 케이스로 테스팅을 수행하면 추가적인 안전성 측정기법이 필요하지 않을 것이다. 우리는 사례연구를 통해 테스트 케이스의 형태에 따른 정형 기법을 정리해 보았으며 신뢰성 있는 시스템을 위한 품질 측정 프레임워크를 (SQAF-DS, Software Quality Assessment Framework for Dependable System) 고안해보았다. SQAF-DS를 이용하여 신뢰성의 다른 중요한 관점들도 테스트 케이스를 통해 측정해보고자 한다. Software safety is one of important principle of dependable software system and also an important dimension of dependability. Safety experts analyze and refine safety requirements of target software system through safety analysis techniques and conduct safety assessment to assure that how the software reflects the safety requirements. Regulation authorities strongly recommend quality demonstration with safety analysis and assessment methods prior to operating permission for dependable system; however the methods are labor intensive and time/cost consuming activities. The thesis proposes a way indirectly assesses safety using test cases to reduce the efforts. We elicit safety properties from minimal cut-sets of software fault trees and find test cases which include the safety properties. Test using the test cases covers the included safety properties, thus we need not additional safety assurance method for the properties. We also conducted case studies that assess safety using test cases. As extension of this approach, we devise software quality assessment framework for dependable system (SQAF-DS). We plan to assess other important dimensions of dependable software systems with the framework.

An Evaluation and Acceptance of COTS software for FPGA-based Controllers in NPPs

정세진 건국대학교 대학원 2016 국내석사

FPGA (Field-Programmable Gate Array)는 PLC (Programmable Logic Controller) 기반의 원자력 발전소 디지털 계측제어 시스템의 대체 플랫폼으로 많은 관심을 받고 있다. FPGA 개발의 software 관점 에서는 합성도구, 배선 및 배치 (Place & Route) 도구와 같은 다양한 상용 소프트웨어들이 사용 된다. 상용 소프트웨어를 원자력 발전소 시스템 개발에 사용하기 위해서는 반드시 EPRI NP-5652/TR-106439와 같은 상용 인증 가이드라인에 의해 dedication 되어야 한다. 하지만 EPRI TR-1025243에서 상용 소프트웨어 인증의 여러 가이드라인 제시 등 노력에도 불구하고 개발에 사용되는 간접사용 소프트웨어의 인증에 대해서는 여러 논란이 되고 있다. 본 논문에서는 발전소 등에 직접 사용되는 상용 제품 이외의 상용 소프트웨어에 대한 인증 프로세스와 평가에 대해 제안 한다. 특히, 본 논문에서 제안하는 인증 프로세스 및 평가는 간접 사용 소프트웨어를 포함하고 또한 평가 기준에 따른 채택 방법 (Verification and Validation techniques)을 제공 한다. 본 논문에서 제안하는 인증 프로세스 및 평가 기준을 이용하여 한국에서 FPGA 기반 디지털 계측제어 시스템 개발에 사용하는 FPGA 합성 도구를 대상으로 적용하여 평가를 진행 하였다. FPGA (Field-Programmable Gate Array) has received much attention from nuclear industry as an alternative platform of PLC (Programmable Logic Controller)-based digital I&Cs (Instrumentation & Control). Software aspect of FPGA development encompasses several commercial tools such as logic synthesis and P&R (Place & Route). The commercial tools which are used to develop nuclear power plant systems should be developed by appropriate standards or dedicated in accordance with domestic standards based on EPRI NP-5652/TR-106439. Even if a state-of-the-art supplementary EPRI TR-1025243 makes an effort, the dedication of indirect COTS (Commercial Off-The-Shelf) SW such as FPGA logic synthesis tools has still caused a dispute. This paper proposes an acceptance process and evaluation criteria, specific to COTS SW, not commercial-grade direct items. It specifically incorporates indirect COTS SW and also provides categorized evaluation criteria for acceptance. It provides an explicit linkage between acceptance methods (Verification and Validation techniques) and evaluation criteria, too. We tried to perform the evaluation and acceptance process step by step upon a commercial FPGA logic synthesis tool being used to develop a new FPGA-based digital I&C in Korea, and could confirm its applicability.

A Study on Identification of Quality Attribute Scenario for Safety of Cooperating Cyber-Physical Systems Using Systems-Theoretic Process Analysis

Yoona Heo 건국대학교 대학원 2023 국내석사

Cyber-Physical System (CPS) is a real-time system which computation, communication, and control parts are integrated and deals with the physical world. CPSs such as unmanned aerial vehicles, automotive vehicles, and smart grids are safety-critical since those CPSs perform safety-critical tasks. A lot of research has been done by many researchers to achieve the safety of individual CPSs. Meanwhile, CPSs can cooperate to achieve a common goal and safety is one of the emergent properties that can appear while systems cooperate. Therefore, not only the safety of each safety-critical CPS but also the safety of an overall CPS, which is composed of various heterogeneous CPSs, must be achieved to a sufficient level. Safety is one of the Quality Attributes, which are measurable or testable non-functional properties of a system to indicate how well the system meets the needs of stakeholders beyond the basic functions of the system. Requirements for such Quality Attributes can be specified in a form of a scenario, called Quality Attribute Scenarios (QASs). Identifying QASs is an effective way to show whether Quality Attribute Requirements have been met. If the requirement or design specifications of the system are complemented by the identified QASs, it can be objectively demonstrated that a system satisfies a quality attribute requirement enough, since the system will be implemented satisfying such requirements and design specifications. This paper proposes an approach to identify QASs for the safety of an overall CPS composed of cooperating safety-critical constituent CPSs using causal scenarios from a state-of-the-art hazard analysis technique, Systems-Theoretic Process Analysis (STPA). We also applied the proposed approach to a case study of an example of two types of CPS which has interactions to achieve a common goal, to demonstrate that by using this proposed approach, requirements and/or design specifications of cooperating CPSs can be complemented from the perspective of safety. 가상물리시스템은 계산, 통신, 그리고 제어 총 세 가지 부분이 통합되어 있고 물리적인 세계를 다루는 실시간 시스템이다. 무인 항공기, 자율주행 자동차, 스마트 그리드와 같은 가상물리시스템들은 안전이 중요한 작업들을 수행하기 때문에 safety-critical하다. 그리고 이러한 개별 CPS의 안전성을 달성하기 위한 많은 연구들이 진행되어 왔다. 한편, CPS는 공동의 목표를 달성하기 위하여 협업할 수 있고, 안전성은 시스템이 협업할 때 나타날 수 있는 emergent한 특성 중 하나이다. 그러므로, 각각의 safety-critical한 CPS의 안전성 뿐 아니라 다양한 서로 다른 종류의 CPS들로 구성된 전체 CPS의 안전성까지도 충분한 수준으로 달성되어야 한다. 안전성은 품질 특성의 일종으로, 품질 특성은 시스템이 이해 관계자의 요구를 얼마나 잘 충족하는 지를 나타내기 위한 측정 가능하거나 테스트 가능한 시스템의 비기능 특성이다. 이러한 품질 특성의 요구사항은 시나리오의 형태로 구체화될 수 있는데, 이것을 품질 특성 시나리오라고 부른다. 품질 특성 시나리오를 식별하는 것은 품질 특성 요구사항이 만족되었는지를 보여주기 위한 효과적인 방법이다. 시스템은 요구사항과 설계 명세를 만족시키도록 구현될 것이므로, 요구사항 또는 설계 명세가 식별된 품질 특성 시나리오를 활용하여 보완된다면 시스템이 품질 특성 요구사항을 충분히 만족시킴을 객관적으로 보일 수 있다. 본 논문에서는 최신 위험 분석 기법인 STPA를 활용하여 안전 중요 가상물리시스템이 협업하여 만들어지는 전체 가상물리시스템의 안전성에 대한 품질 특성 시나리오를 식별하기 위한 방법을 제안한다. 또한, 공동의 목표를 달성하기 위해 상호작용하는 두 종류의 가상물리시스템의 예시를 활용한 사례 연구에 본 논문에서 제안한 접근 방식을 사용함으로써 협력하는 가상물리시스템의 요구사항과 설계 명세가 안전성의 관점에서 보완될 수 있음을 보인다.

A Formal Verification Framework using Traceability-based Selective Model Projection for Large-scale Software

이동아 건국대학교 대학원 2019 국내박사

정형 검증 기법중 하나인 모델체킹은 안전 필수 시스템의 기능 정확성(functional correctness)를 확인하기 위하여 널리 사용되는 기법이다. 모델 체킹을 다루는 연구는 비교적 작은 규모의 소프트웨어를 대상으로 한다. 운영체제와 같이 크고 복잡한 시스템 전체를 모델체킹으로 검증하는 것은 불가능에 가깝다. 일반적으로 모델체킹을 사용하여 규모가 큰 시스템을 검증하고자 할 때는 소프트웨어를 기능이나 모듈 단위로 나눠서 검증을 수행한다. 하지만 단순하게 나눠진 기능이나 모듈을 검증한 결과는 소프트웨어 전체를 실행했을 때 발생할 수 있는 기능적 결함을 찾아내기는 어렵다. 따라서 대규모 소프트웨어를 대상으로 모델체킹을 수행하고자 할 때, 대상을 목적에 맞게 나누는 방식이 가장 중요하다. 본 논문에서는 추적성을 기반으로 검증 목적에 관련되는 소프트웨어의 특정 부분을 체계적으로 찾아낼 수 있는 선택적 모델 투영(Traceability-based Selective Model Projection) 기법과, 그 기법을 활용하여 대규모 소프트웨어의 정형검증을 수행하기 위한 프레임워크를 제안한다. 프레임워크를 사용해 검증을 수행하기 위해서는 소프트웨어 개발산출물 간의 추적성을 확보하는 것이 선행되어야 한다. 확보된 추적성을 바탕으로 소프트웨어를 수평적 관점 및 수직적 관점으로 모델링 및 검증을 수행한다. 수평적 관점은 소프트웨어 전체를 대상으로 넓고 얕은 모델을 생성하기 위한 관점이며, 수직적 관점은 검증 목적에 초점을 맞춰 소프트웨어의 특정 부분을 상세하게 다루기 위한 관점이다. 제안하는 선택적 모델 투영 기법은 수평적 관점으로 생성한 소프트웨어의 모델을 검증 목적에 맞게 시뮬레이션하고, 시뮬레이션 과정에서 활성화되는 영역을 도출하여 모델의 특정 영역을 도출한다. 모델 투영을 통해 도출한 수평적 모델의 특정 부분은 추적성을 활용해 소스코드와의 관계를 분석한다. 도출된 소스코드로부터 수직적 모델을 생성하고 모델 투영 과정에서 사용된 검증 목적을 사용해 수직적 검증을 수행한다. 제안하는 프레임워크를 사용하여 항공용 실시간 운영체제인 Qplus-AIR를 대상으로 정형검증을 수행하였다. 검증을 위하여 Qplus-AIR가 준수하는 ARINC 653-1 표준으로부터 검증 속성을 도출하였으며, 수평적 관점으로 시스템의 모델을 생성하기 위하여 Statemate를 사용하였다. 투영된 수직적 관점의 모델을 검증하기 위하여 3가지 (SPIN, Times, CBMC) 모델체커를 사용하였다. 사례연구를 통해 제안하는 검증 프레임워크가 대규모 소프트웨어를 검증하기에 적합함을 확인하였다. 또한 밝혀낸 Qplus-AIR의 문제점과 이를 해결하기 위한 방법을 개발팀에 보고하여 개선할 수 있도록 하였다. Model checking, one of formal verification techniques, is widely accepted as a useful technique to demonstration of functional correctness for software in safety critical systems. Most studies in application of the model checking have handled a relatively small example which has small amount of state space. Large and complex software, such as operating systems, is hardly possible to be verified as a whole, because model checking has limitation about size and complexity of the model. Although it is possible to apply model checking to the software divided into small parts by a function or a module, the simple division is not enough to verify the functional correctness of them working together. Therefore, identifying all parts of software relevant to the verification purpose is important for the verification using model checking. This dissertation suggests a formal verification framework using selective model projection based on traceability to identify specific parts of software with respect to verification purposes. The framework starts with establishing traceability between products of a software development process. Two verification approaches, a horizontal verification and a vertical verification, conduct modeling and verifying the software. The former models and verifies the software in a wide and shallow point of view which covers a wide range of the software but does not include detail information. The latter, on the other hand, models and verifies the software in a narrow and deep point of view which focuses on a specific parts according to a verification purpose. The selective model projection is a technique to identify relevant parts in source code with respect to a verification purpose for the vertical verification. The projection identifies relevant parts through simulating the model for the horizontal verification with a simulation scenario about a verification purpose. Traceability analysis leads to find the parts in source code that corresponds to the projected parts in the model for the horizontal verification. The parts of source code are modeled and verified in the vertical verification. This dissertation shows that a case study about verification of Qplus-AIR, which is a real-time operating system for avionics, demonstrates feasibility of the proposed framework. Verification properties are derived from the standard specification, ARINC 653-1 which Qplus-AIR complies. Modeling and verification of Qplus-AIR for the horizontal verification uses Statemate, and it checks whether the Statemate model satisfies the properties using a model checker and a simulator. Three model checkers, SPIN, Times, CBMC, are selected to verify models for the vertical verification. The result of the case study demonstrated the feasibility of the framework, and the verification found some property violations which were delivered to the development team.

A Comprehensive Relationship Analysis for Heterogeneous Artifacts in Multiple-Collaborative Safety-Critical Systems

정세진 건국대학교 대학원 2022 국내박사

Multiple-collaborative safety systems produce heterogeneous artifacts from development and safety analysis on each constituent system, and such artifacts show diverse and complex relationships. Therefore, it is necessary to analyze the connectivity/traceability relationships of such artifacts in multiple systems thoroughly. This dissertation proposes a comprehensive relationship analysis of artifacts of multiple-collaborative safety-critical systems with a traceability-based connectivity relationship analysis framework, “ARTracer.” The proposed framework receives heterogeneous artifacts and can analyze connectivity relationships. Furthermore, it generates focused relationship models by trace operations and semantic analysis for supporting life cycle activities effectively. 다중 협업 안전 시스템은 여러 종류의 구성 시스템들로 구성된 시스템으로 개발 및 안전성 분석에서 이종의 산출물 들이 도출된다. 이러한 산출물들은 복잡하고 다양한 연결 관계를 가질 수 있으며 시스템의 협업 관계에 따라서도 연결성을 갖게 된다. 여러 기존 연구들에서 다양한 추적성 분석 방법, 모델들을 제안하고 있지만, 다중 협업 시스템의 연결 관계를 포함한 개발 산출물 및 안전성 분석 산출물의 복합적인 관계 분석에 대해서는 부족한 점이 있다. 본 논문에서는 다중 협업 시스템의 다양한 산출물간 복합적인 관계 분석을 위해 추적성을 기반으로 하는 연결성 분석 프레임워크인 ARTracer를 제안한다. 본 논문에서 제안하는 프레임워크는 산출물 입력 및 관리, 연결관계 분석, trace operation 과 그 조합을 통한 관계 모델 생성의 단계로 구성된다. 각 산출물의 추적/연결 관계 분석을 위해 제안하는 프레임워크 에서는 개발 및 안전성 분석 산출물을 입력으로 받아 추상화된 모델로 변환 및 관리한다. 연결 관계 분석은 제안한 모델의 각 요소를 연결하는 것으로 진행되며, 연결의 의미에 따라 연결 타입을 제공한다. 또한 trace operation 및 trace operation의 조합을 통한 semantic analysis를 통해 분석한 연결 관계를 추출하여 목적에 맞게 추출된 관계 모델을 생성한다. 또한, 제안하는 프레임워크 및 분석 방법의 적용 가능성을 확인하기 위해 돌발 상황 검지 시스템 과 군집 주행 시스템의 각 산출물을 이용하여 사례 연구를 수행하였다.

OOPT manager : 교육용 개발 방법론의 추적성 기반 산출물 통합 관리 프레임워크

김민우 건국대학교 2019 국내석사

소프트웨어 공학 수업에서 활용하는 OOPT(Object-Oriented Process with Traceability)는 교육용 소프트웨어 개발 방법론으로서, 각 개발 단계마다 필요한 요구사항과 산출물을 구체적이고 명확하게 정의하고 있다. OOPT는 추적성 기반 객체 지향 개발 방법론으로 계획 초기의 요구사항부터 분석, 설계, 구현, 테스팅까지의 개발과정에서 생산되는 산출물들의 관계를 추적성에 따라 정의할 수 있는 특징을 갖고 있다. 산출물 간의 추적성 분석을 통해 개발된 시스템이 요구사항에 잘 부합했는지 확인할 수 있고, 개발과정에서 변경사항이 발생했을 경우에도 개발 전체과정의 일관성을 유지할 수 있게 된다. 학생들은 수업에서 OOPT 방법론에 따라 개발과정의 각 단계에서 필요한 활동을 적절하게 수행하고, 다양한 형태의 산출물을 문서로 작성한다. 작성된 산출물의 문서는 추적성 분석에 활용되어 소프트웨어를 올바르게 개발하였는지 확인할 수 있다. OOPT의 각 단계를 수행하고, 산출물을 정확하게 문서로 작성해야 한다. 따라서 학생들은 개발단계를 진행하며 반복되는 문서 작성 작업과 정확한 작성에 대한 확인 및 추적성 정의 작업은 많은 시간과 노력을 필요로 한다. 또한, 단계가 점차 진행될수록 다량의 산출물이 생산되기 때문에, 이를 손으로 작성 및 관리하는 것은 매우 많은 시간과 노력을 요구한다. 뿐만 아니라, 개발 과정 중 발생한 변경사항과 관련된 문서가 많을 경우, 일관적인 수정과 관리가 어렵다. 그렇기 때문에 OOPT를 올바르게 수행하였더라도 문서가 정확하지 않다면, 산출물 간의 관계를 분석하는 추적성 분석에 어려움 발생한다. 추가적으로, 시스템이 복잡해지고 개발과정이 진행되어 데이터가 많아질수록 추적성 분석이 쉽지 않게 된다는 문제점도 있다. 이를 위해 본 연구에서는 OOPT 수행의 어려움을 해결하고자 추적성 분석을 위한 모델을 정의하여 추적성 분석 지원에 대한 방법을 제시하고, 제시한 방법과 문서 작성을 위한 템플릿을 제공, 추적성 분석의 자동화를 지원하는 체계적인 수행을 위한 프레임워크를 개발하였다. 프레임워크의 효용성을 확인하기 위해 OOPT를 직접 손으로 수행한 결과와 프레임워크를 통해 수행한 결과를 비교하여 프레임워크가 OOPT 수행에 도움이 되는 것을 확인하였다. Object-Oriented Process with Traceability (OOPT), which is used in software engineering classes, is an educational software development methodology, and it specific and clearly defines requirements and outputs required for each development stage. OOPT is an object-oriented development methodology with traceability. It has the feature that traceability can define the relation of the output produced in the development process from initial requirements to analysis, design, implementation, and testing. By analyzing traceability between artifacts, you can ensure that the developed system meets your requirements and maintain consistency throughout the development process, even if the development process changes. Students perform the necessary activities at each stage of the development process according to the OOPT of the course and document various output types. The resulting output document can be used for traceability analysis to ensure that the software was developed correctly. Students must perform each step of the OOPT and accurately document the output. Therefore, it is time consuming and lots of effort to carry out the development stage, to define the repetitive document creation, to confirm the correct writing, and to define traceability. Also, as the step progresses, a large amount of output is generated, so it takes a lot of time and effort to manually create and manage the output. In addition, if there are a lot of documents related to the changes that have occurred during the development process, it is difficult to make consistent changes and management. Therefore, even if the OOPT is correctly performed, if the document is not accurate, it is difficult to analyze the traceability of analyzing the relationship between the products. Furthermore, there is a problem that the more complex the system becomes and the more developed the data becomes, the more difficult it is to analyze the traceability. In this paper, we propose a methodology to support systematic performance and traceability analysis to solve the difficulty of OOPT, and developed a framework to support the proposed method, repetitive document creation, and automation of traceability analysis. In order to verify the effectiveness of the framework, we compared the results of the manual OOPT with the results of the OOPT using framework, and confirmed that the framework is useful for performing OOPT.

An extended process of STPA and implementation of an automatic assistant tool for reactor protection system software

서영주 건국대학교 대학원 2016 국내석사

The Safety critical system is the system whose mishap or hazard severity consequence is deemed to be either catastrophic or critical. Reactor protection system in nuclear power plant is also included in the safety critical system and the accident of this system makes critical damage. Therefore, to reduce the damage of the accident of the system, many hazard analysis techniques are developed and applied. In previous years, the hazard analysis techniques based on Chain-of-failure event causality model like Fault tree analysis or Failure Mode and effects Analysis were mainly used for hazard analysis. However, recent research indicates that the use of computers and other new technology has allowed increasingly complex design and traditional hazard analysis techniques are not suitable for hazard of these systems. As a result, STAMP/STPA which based on the system-theoretic accident model was proposed for the effective analysis of recent complex system. However, STPA is designed for system level hazard analysis and does not treat implementation details like software implementation. But problems in implementation details are important because it also can lead to an accident. Therefore, this paper purpose hazard analysis process of software operation based on STPA and software formal specification to find out the hazard of software operation. After then, we applied this process to the software of nuclear power plant reactor protection system to show the feasibility. 안전 필수 시스템이란 시스템의 동작에서 사고가 발생할 경우 인명피해나 환경파괴 같은 큰 피해를 줄 수 있는 시스템을 말한다. 원자력 발전소의 원자로 보호 시스템 또한 이러한 안전 필수 시스템에 속하며 사고가 발생할 경우 주위에 큰 피해를 주게 된다. 따라서 이러한 안전 필수 시스템의 사고로 인한 피해를 줄이기 위해 이를 대상으로 한 위해도 분석 기법, 프로세스들이 많이 연구되었고 또한 시스템의 위험성을 줄이기 위해 적용되어 왔다. 예전에는 위해도 분석 기법들로 Fault tree analysis나 FMEA와 같은 원인과 결과의 관계를 기반으로 한 모델(Chain-of-failure-event causality model)을 사용하는 기법들이 주로 사용되었지만, 최근 들어 이것 만으로는 점점 복잡해지고 있는 현대의 시스템에서 발생할 수 있는 위해를 찾아내기가 어렵다고 생각되었고, 이를 대상으로 효과적인 분석을 수행하기 위해 STPA라는 기존의 위해도 분석 기법들과 다르게 시스템 이론을 기반으로 한 사고 모델을 사용하는 위해도 분석 기법도 제안되었다. 하지만 STPA는 시스템 레벨을 대상으로 하여 발생할 수 있는 위해를 분석하는 기법이며 소프트웨어의 동작 같은 구현 수준의 정보를 분석 단계에서 자세히 다루지 않는다. 하지만 구현 수준에서 발생하는 문제가 시스템의 사고로 이어질 수 있기 때문에 이에 대한 분석 또한 중요하다. 따라서 본 논문에서는 STPA를 기반으로 하여 소프트웨어의 형식 명세서를 사용하는 것으로 소프트웨어의 동작이 시스템 레벨의 위해에 어떤 영향을 미치는지에 대한 분석을 돕는 프로세스를 제안하며 이를 실제 원자력 발전소의 원자로 보호 시스템 (RPS)의 소프트웨어를 대상으로 적용한 사례와 적용에 대한 결과를 설명할 것이다.

원자력발전소 상용 소프트웨어를 위한 사이버 보안인증 절차 개발

김태현 건국대학교 대학원 2017 국내석사

원자력 발전소는 아날로그로 운영되던 내부 설비가 노후화 등으로 성능 저하가 우려됨에 따라 노후 기기들은 디지털 제품으로 교체되고 있다. 때문에 원자력 발전소에서는 노후화된 PLC 기반의 디지털 계측 제어 시스템을 대신하기 위해 FPGA 기반 시스템이 연구 및 개발되고 있다. FPGA 시스템 개발 단계에서는 합성도구와 같은 다양한 상용 도구들이 사용이 되기 때문에 안전을 최우선으로 하는 원자력 발전소에서 원자력품질 프로그램 하에 생산되지 않은 상용 도구들을 사용하기 위해서는 EPRI NP-5652/TR-106439와 같은 상용 제품 인증 지침으로 검증해야 한다. 하지만 이러한 인증 규정들에는 일반 산업 제어 시스템에서 필수적으로 언급하고 있는 사이버 보안에 대한 내용이 언급되고 있지 않다. 최근 원자력 발전소의 시설들은 자체적으로 외부와 분리되어 있고, 독립적이고 폐쇄적인 환경이어서 외부의 보안 위협으로부터 안전하다고 생각하였다. 하지만 최근 이란 원자력 발전소에서 발견된 스턱스넷 악성 코드로 인해 더 이상 원자력 발전소도 사이버 공격에 안전지대가 아니라는 것이 증명 되어서 사이버 보안이 필수적으로 요구되고 있다. 본 논문에서는 원자력 발전소 계측 제어 시스템 개발에 사용되는 상용 제품 인증에 보안 항목을 추가하여 상용 도구를 이용한 계측 제어 시스템 개발에 보안성을 향상 시킬 수 있는 보안인증 절차를 제시한다. Nuclear power plants are undergoing the replacement of obsolete components with digital products due to the concerns about decreased performance by aging internal analog products. Therefore, FPGA-based systems are being researched and developed to replace the obsolete PLC-based digital Instrumentation and Controller in nuclear power plants. Commercial tools such as Synthesis tool that used in FPGA system development stage are not produced under nuclear quality assurance in nuclear power plants where safety is the top priority. Therefore commercial grade item dedication process such as EPRI NP-5652/TR-106439 is required. However, these certification rules do not mention cyber security, which is an essential part in the industry control system. Recently, Nuclear power plant facilities are separated from the outside and are considered to be safe from external security threats because of its independent and closed environment. However, due to Stuxnet malicious code detected recently from Iranian nuclear power plant, it has been proved that the nuclear power plants are no longer in the safety zone from cyber-attacks; therefore cyber security is necessarily required. In this paper, Adding security criteria to COTS SW, which is used for the development of nuclear power plant instrumentation and controller system, the security certification process that can improve the security of developing instrumentation and controller system using commercial tools is suggested.

An Operational Semantics for Simulating NuSCR Formal Specifications

손준익 건국대학교 대학원 2019 국내석사

Rigorous verification & validation of software through formal method is highly recommended when developing a safety critical system like a digital protection system in a nuclear power plant (NPP). Various formal specification-based verification techniques, such as testing, simulation and model checking, have been proposed to verify and validate the specifications. This paper describes the foundation and tool to support simulation of the software requirements written in NuSCR formal specification language. We have defined an operational semantics for NuSCR language based in natural semantics and simulation engine algorithms for NuSCR Software System (NSS) which is a symbolic executable model of the software system written in NuSCR. The operational semantics and simulation engine algorithms have been implemented as a simulator – “NuSCRSim”. It provides an visual animation of the NuSCR constructs, which makes it easier to directly check the behavior of a model. We also performed a case study with examples of the APR-1400 nuclear reactor protection system in Korea in order to demonstrate of the correctness of the “NuSCRSim”. 원자력 발전소의 디지털 보호 시스템과 같이 안전 필수 시스템에 들어가는 소프트웨어를 개발할 때는 정형 기법을 통한 소프트어의 엄격한 검증 및 확인이 권장된다. 이에 따라, 요구사항 단계에서 테스트, 시뮬레이션 및 모델 체킹과 같은 다양한 정형 명세 기반 검증 기술이 제안되었다. 본 논문에서는 NuSCR 정형 명세 언어로 작성된 소프트웨어 요구 사항의 시뮬레이션을 지원하기 위한 기초이론과 이론을 구현한 시뮬레이터 도구를 제안한다. 먼저 시뮬레이션을 하기 위한 기반이론이 되는 NuSCR 언어의 동작 시맨틱을 Natural Semantic 방법을 기반으로 정의하였고 NuSCR로 작성된 소프트웨어 시스템의 실행 모델인 NSS (NuSCR 소프트웨어 시스템)의 특성에 맞춰 시뮬레이션 엔진을 정의하였다. 해당 동작 시맨틱 및 시뮬레이션 엔진은 NuSCR로 작성된 정형 명세를 시뮬레이션 할 수 있는 시뮬레이터인 “NuSCRSim” 으로 구현되었다. 해당 도구는 NuSCR 구조의 시각적인 애니메이션을 제공하여 모델의 동작을 쉽게 이해할 수 있게 도와준다. 우리는 또한 해당 시뮬레이터의 정확성을 입증하기 위해 APR-1400 원자로 보호 시스템의 하나의 모듈을 이용하여 시험을 수행하였다.

Verification of Behavioral Consistency between FBD and C programs using HW-CBMC

이동아 건국대학교 대학원 2012 국내석사

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. 원자력 발전소나 철도, 비행기 등과 같은 안전필수시스템은 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모델의 일부 모듈을 사용해 검증을 수행한 결과를 기술하였다.