융합소프트웨어 안전성을 위한 소프트웨어공학 기술 적용

차성덕(Sungdeok Cha),최진영(Jinyoung Choi),김선한(Seonhahn Kim),이희조(Heejo Lee),장길수(Gilsoo Jang),남원홍(Wonhong Nam),최재순(Jaesoon Choi),이정주(Jungjoo Lee),정세훈(Sehun Jeong),황대연(Daeyon Hwang),송경섭(Kyungsub Song),신병윤(Bye 한국정보과학회 2010 정보과학회지 Vol.28 No.2

PVS를 이용한 SCR 스타일의 소프트웨어 요구사항 명세에서 기능 요구 사항의 정형 검증

김태호(Taeho Kim),차성덕(Sungdeok Cha) 한국정보과학회 2002 정보과학회 컴퓨팅의 실제 논문지 Vol.8 No.1

소프트웨어의 개발 단계 중 품질을 결정하는 주요 단계는 요구 명세 단계로 알려져 있다. 따라서, 소프트웨어 개발 업체는 소프트웨어 요구명세의 분석을 가장 중요한 단계 중 하나로 취급하고 있고, 특히 안전성이 중요한 시스템의 경우에는 시스템을 운영하기 위하여 국내와 국제적인 규제 기관에서는 요구 명세의 분석을 통한 안전성의 입증을 요구한다. 소프트웨어의 요구 명세 분석을 위한 방법 중 인스펙션과 정형 검증이 가장 효과적인 방법으로 알려져 있다. 본 논문에서는 SCR-style의 요구 명세를 정리 증명기인 PVS를 이용하여 정형 검증을 수행하는 방법을 제안하였다. 그리고, 논문에서 제안된 방법으로 실제 월성 원자력 발전소의 정지 시스템의 검증을 수행하였다. 이 시스템은 인스펙션으로 검증된 적은 있으나 정형 검증 방법으로는 증명된 적이 없고, 국내에서 실제 운영되는 산업계시스템에 정형 검증 방법이 적용된 사례는 매우 드물기 때문에 차후 정형 검증 방법을 적용하기 위한 평가로서도 이와같은 실험적인 적용이 매우 중요하다. Among the many phases involved in software development, requirements analysis phase is generally considered to play a crucial role in determining the overall software quality. Therefore, many software development companies manages the phase as one of the important phase. Especially, safety assurance through requirements analysis for safety-critical systems is quite demanding, and national and international bodies routinely require safety demonstration. Among various approaches, inspection and formal methods are generally shown to be effective. In this paper, we propose a formal verification procedure for SCR(Software Cost Reduction)-style SRS (Software Requirements Specification) using the PVS specification and verification procedure and applied this procedure to an industrial system such that a shutdown system for Wolsung nuclear power plant. This system had been verified through inspection not formal verification. The application of formal methods is rare in Korea, so it is very important to experiment about formal verification to industrial systems.

정형 소프트웨어 요구사항으로부터 PLC 디자인의 체계적 생성

유준범(Junbeom Yoo),차성덕(Sungdeok Cha),김창회(Chang Hui Kim),송덕용(Deokyong Song) 한국정보과학회 2005 정보과학회논문지 : 소프트웨어 및 응용 Vol.32 No.2

원자력 발전소의 디지털 제어 시스템은 안전성이 중요시되는 safety-critical 소프트웨어로서 충분한 수준의 안전성을 보장하기 위해서 여러 기법들이 적용되고 있다. 특히, 정형명세 기법은 개발의 초기 단계에서 소프트웨어 요구 사항들을 명확하고 완전하게 명세하도록 유도함으로써 안전성을 크게 향상시킬 수 있는 기법으로 인정받고 있다. 본 논문에서는 정형명세 기법인 NuSCR을 이용해서 작성된 요구사항 명세로부터, 설계 단계의 내용으로 사용될 수 있는 PLC 기반의FBD 프로그램을 체계적으로 생성하는 기법을 제안하고 있다. 제안된 기법은 기존의 수동 명세 작업에서 발생할 수 있는 오류들을 크게 줄일수 있으며, 소프트웨어의 개발 비용과 기간을 줄일 수 있다. 또한, 제안된 기법의 유용성을 증명하기 위해서, 현재 KNICS에서 개발 중인 DPPS RPS의 BP를 구성하는 트립 논리 중의 하나인 고정 설정치 상승트립을 예제로 설명하고 있다. The software of the nuclear power plant digital control system is a safety-critical system where many techniques must be applied to it in order to preserve safety in the whole system. Formal specifications especially allow the system to be clearly and completely specified in the early requirements specification phase, therefore making it a trusted method for increasing safety. In this paper, we discuss a systematic method, which generates PLC-based FBD programs from the requirements specification using NuSCR, a formal requirements specification method. This FBD programs takes an important position in design specification. The proposed method can reduce the possible errors occur in the manual design specification, and the software development cost and time. To investigate the usefulness of our proposed method, we introduce the fixed set-point rising trip example, a trip logic of BP in DPPS RPS, which is presently being developed at KNICS.

Active Timeout 을 이용한 SYN Flooding 공격의 해결

서정석(Jeongseok Seo),차성덕(Sungdeok Cha) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.2Ⅰ

서비스 거부(denial of service) 공격의 일종인 SYN flooding 공격은 TCP/IP 프로토콜의 오류로 인해 발생한다. 기존의 SYN flooding 해결 연구들은 대부분 방화벽이나 라우터에서 패킷을 감시하여 불법적으로 판단된 패킷을 걸러내는 방법을 사용하였다. 따라서 기존의 연구들은 방화벽이나 라우터에 많은 부하를 주게 된다. 본 연구에서는 방화벽이나 라우터의 도움을 받지 않고, 기존의 네트워크 환경이나 운영체제에 큰 변화를 가하지 않으면서, 서버 시스템 자체만으로 SYN flooding 공격에 효율적으로 대응할 수 있는 방법을 제시하고자 한다.

디지털 원자로 보호 시스템을 위한 정형 소프트웨어 요구사항 명세

유준범(Junbeom Yoo),차성덕(Sungdeok Cha),김창회(Chang Hwoi Kim),오윤주(Younju Oh) 한국정보과학회 2004 정보과학회논문지 : 소프트웨어 및 응용 Vol.31 No.6

원자력 발전소의 디지털 제어 시스템에 적용되는 소프트웨어는 안전성이 중요시되는 safety-critical 소프트웨어로, 충분한 수준의 안전성을 보장하기 위해서 여러 기법들이 적용되고 있다. 특히, 정형명세 기법은 개발의 초기 단계에서 소프트웨어 요구 사항들을 명확하고 완전하게 명세하도록 유도함으로써 안전성을 크게 향상시킬 수 있는 기법으로 인정 받고 있다. 본 논문에서는 원자력 발전소 디지털 제어 시스템 소프트웨어의 요구 사항 명세에 적합하도록 개발된 정형명세 기법인 NuSCR을 논의한다. 또한, 개발된 NuSCR의 적용성을 검토하기 위해, 현재 KNICS 사업단에서 개발중인 발전소보호계통 소프트웨어의 요구사항을 정형 명세한 경험을 소개하고 있다. 또한, 원자력 도매인에 특화된 정형명세 기법인 NuSCR의 우수성도 실례를 들어 설명하고 있다. The software of the nuclear power plant digital control system is a safety-critical system where many techniques must be applied to it in order to preserve safety in the whole system. Formal specifications especially allow the system to be clearly and completely specified in the early requirements specification phase therefore making it a trusted method for increasing safety. In this paper, we discuss the NuSCR, which is a qualified formal specification method for specifying nuclear power plant digital control system software requirements. To investigate the application of NuSCR, we introduce the experience of using NuSCR in formally specifying the plant protection system’s software requirements, which is presently being developed at KNICS. Case study that shows that the formal specification approach NuSCR is very much qualified and specialized for the nuclear domain is also shown.

MAPPING TABLE TABLE을 이용한 금융 PRODUCT FACTORY 분석기법

박진희(Jinhee Park),유준범(Junbeom Yoo),차성덕(Sungdeok Cha) 한국정보과학회 2009 한국정보과학회 학술발표논문집 Vol.36 No.1

금융 Product factory는 금융상품 구성을 위한 각 컴포넌트들을 정의하고, 상품개발이 필요할 때 필요한 컴포넌트를 조합하여 쉽고 빠르게 상품을 개발할 수 있도록 지원하는 시스템을 말한다. 이와 같은 시스템의 구축을 위해서는 분석, 설계자의 상품에 대한 통찰력과 함께, Legacy System을 효율적으로 분석하여 Rule과 데이터로 모델링 할 수 있는 방법이 필요하다. 본 논문은, Legacy system의 분석정보를 Mapping Table로 데이터화하여, factory 모델링 대상 정보를 체계적으로 분석하고 분류하는 방법을 제시하였다. 또한, 국내 금융기관의 분석기법 적용사례를 통하여 본 연구의 구현효과를 검증하였다.

함수 블록 다이어그램으로 구현된 PLC 프로그램에 대한 정형검증

지은경(Eunkyoung Jee),전승재(Seungjae Jeon),차성덕(Sungdeok Cha) 한국정보과학회 2008 한국정보과학회 학술발표논문집 Vol.35 No.1

NuSCR 정형 요구사항명세로부터 FBD 프로그램 자동생성을 위한 도구(NuSCRtoFBD) 개발

백형부(Hyoungbu Back),유준범(Junbeom yoo),차성덕(Sungdeok Cha) 한국정보과학회 2008 한국정보과학회 학술발표논문집 Vol.35 No.2

템플릿에 기반한 NuSCR 정형 명세의 소프트웨어 고장 수목 생성 방법

김태호(Taeho Kim),유준범(Junbeom Yoo),차성덕(Sungdeok Cha) 한국정보과학회 2005 정보과학회논문지 : 소프트웨어 및 응용 Vol.32 No.12

본 논문은 NuSCR 정형 명세 언어로 작성된 소프트웨어 요구 명세로부터 소프트웨어 고장 수목을 생성하는 방법에 대하여 제안하였다. 본 연구에서 제안하는 소프트웨어 고장 수목은 소프트웨어의 구조와 동작에 대한 요구 사항을 반영하는 통합된 형태의 고장 수목으로, 안전성에 대한 복합적인 분석이 가능하다. 이러한 소프트웨어 고장 수목을 생성하기 위하여 NuSCR 정형 명세언어의 구성 요소 각각에 대한 템플릿을 정의하고, 이들 템플릿을 사용하여 소프트웨어 고장 수목을 생성하는 방법을 제안하였다. 그리고, 제안된 방법의 유용성을 평가하기 위해 현재 국내 원전계측제어시스템 개발사업단에서 개발 중인차세대 원자력 시스템 APR1400에 사용될 원자로 보호 시스템의 핵심 트립 논리에 대하여 고장 수목을 생성하고 분석 하였다. In this paper, we propose a synthesis method of software fault tree from software requirements specification written in NuSCR formal specification language. The software fault tree, proposed in this paper, reflects requirements on both structure and behavior and it is an integrated form. The software fault tree can be used for analyzing safety in the view of structure and behavior. We propose templates for each components in NuSCR specification language and a synthesis method of software fault tree using the templates. The research was applied into the main trip logic of the reactor protection system of ARP1400, the Korean next generation nuclear reactor system, developed by KNICS. And we evaluate feasibility of our approach through this case study.

함수 블록 다이어그램으로 구현된 PLC 프로그램에 대한 정형 검증 기법

지은경(Eunkyoung Jee),전승재(Seungjae Jeon),차성덕(Sungdeok Cha) 한국정보과학회 2009 정보과학회 컴퓨팅의 실제 논문지 Vol.15 No.3

프로그래머블 로직 콘트롤러(PLC)가 원자력 계측제어 시스템과 같은 안전 필수 시스템 구현에 많이 사용됨에 따라, PLC 프로그램에 대한 정형검증의 필요가 높아지고 있다. 본 연구에서는 함수 블록 다이어그램(FBD)으로 구현된 PLC 프로그램에 대한 자동화된 정형검증 기법을 제안한다. FBD 프로그램을 검증하기 위해서 먼저 FBD 프로그램을 검증언어인 Verilog로 변환하고, 변환된 Verilog 모델에 대해 SMV 모델체커를 호출해 모델체킹을 수행한다. 자동화를 위해 FBDVerifier 도구를 개발하였다. FBD Verifier는 FBD 프로그램으로부터 Verilog 모델로의 자동변환 기능뿐 아니라 모델체킹 결과 생성된 반례를 직관적이고 효과적으로 분석할 수 있는 기능 또한 제공한다. 제안된 기법과 도구를 사용해 원전계측제어시스템 개발사업단의 원자로 보호시스템에 대한 방대한 양의 FBD 프로그램을 성공적으로 검증하였다. As Programmable Logic Controllers (PLCs) are increasingly used to implement safety critical systems such as nuclear instrumentation & control system, formal verification for PLC based programs is becoming essential. This paper proposes a formal verification technique for PLC program implemented with function block diagram (FBD). In order to verify an FBD program, we translate an FBD program into a Verilog model and perform model checking using SMV model checker. We developed a tool, FBDVerifier, which translates FBD programs into Verilog models automatically and supports efficient and intuitive visual analysis of a counterexample. With the proposed approach and the tool, we verified large FBD programs implementing reactor protection system of Korea Nuclear Instrumentation and Control System R&D Center (KNICS) successfully.