http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
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.
Active Timeout 을 이용한 SYN Flooding 공격의 해결
서정석(Jeongseok Seo),차성덕(Sungdeok Cha) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.2Ⅰ
서비스 거부(denial of service) 공격의 일종인 SYN flooding 공격은 TCP/IP 프로토콜의 오류로 인해 발생한다. 기존의 SYN flooding 해결 연구들은 대부분 방화벽이나 라우터에서 패킷을 감시하여 불법적으로 판단된 패킷을 걸러내는 방법을 사용하였다. 따라서 기존의 연구들은 방화벽이나 라우터에 많은 부하를 주게 된다. 본 연구에서는 방화벽이나 라우터의 도움을 받지 않고, 기존의 네트워크 환경이나 운영체제에 큰 변화를 가하지 않으면서, 서버 시스템 자체만으로 SYN flooding 공격에 효율적으로 대응할 수 있는 방법을 제시하고자 한다.
정형 소프트웨어 요구사항으로부터 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.
디지털 원자로 보호 시스템을 위한 정형 소프트웨어 요구사항 명세
유준범(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.
함수 블록 다이어그램으로 구현된 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.
신모범(Mo Bum Shin),유준범(Junbeom You),차성덕(Sungdeok Cha) 한국정보과학회 2005 한국정보과학회 학술발표논문집 Vol.32 No.1
원자력 발전소의 제어 시스템은 safety-critical 소프트웨어로서 안정성이 중요시 되는 시스템이다. 최근 기존의 시스템이 PLC 기반의 디지털 제어장치로 대체되면서 이에 사용되는 소프트웨어의 안정성과 품질을 보장하기 위한 경험검증 기법이 요구되고 있다. 특히 PLC 프로그램의 설계에 사용되는 FBD의 모델체킹을 통한 정형검증에 대한 연구는 미비한 수준이다. VIS 검증기는 위의 요구에 부합하는 도구로서 이를 사용하면 여러 종류의 정형 검증이 가능하다. 본 논문에서는 VIS를 이용한 FBD의 검증을 위해서 FBD를 Verilog로 변환 하는 기법을 제안한다. 제안하는 방법의 효율성을 검증하기 위해서 현재 KNICS 사업단에서 개발중인 APR 1400용 원자로 보호 시스템의 운전정지회로들 예로 사용하였다.