http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
박사천(SaChoun Park),이정림(Jungrim Lee),권기현(Gihwon Kwon) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.2Ⅱ
현재 정보보호시스템의 에러로 많은 피해를 입고 있다. 특히 고 보안성이 요구되는 시스템에서의 정보 누출이 심각한 문제가 되고 있는데 이러한 시스템의 예로 스마트카드가 있다. 스마트카드는 오랜 시간 축적된 경험과 연구로써 그 보안성이 특히 우수하다고 할 수 있다. 그러나 애플리케이션 내에서 그리고 애플리케이션 차원에서 보안적 정보흐름을 검사하는 연구들이 많이 진행되어 왔고 자동도구인 모델체커를 이용하는 연구들도 점차 증가하고 있다. 이런 연구들의 연장선상에서, 본 논문에서는 SMV 모델체커를 이용해 자바 바이트코드에 대한 정보흐름의 보안성을 검사하는 방법을 보인다.
병행성 분석을 위한 액션 기반의 LTS 바운드 모델 체커
박사천(Sachoun Park),권기현(Gihwon Kwon) 한국정보과학회 2008 정보과학회논문지 : 소프트웨어 및 응용 Vol.35 No.9
병행 컴포넌트를 포함하는 소프트웨어는 디버깅하기가 매우 어렵다. 따라서 철저하면서도 자동화된 검증 도구의 사용이 필수적이다. 이러한 도구 개발의 노력 중 하나가 바운드 모델 체킹 도구이다. 바운드 모델 체킹은 주어진 바운드 k 안에서 시스템의 실행 경로에 에러가 존재하는지를 철저히 검사한다. 본 논문에서는 LTS로 모델링 된 병행 프로그램을 검증하는 바운드 모델 체킹 도구를 소개한다. 이 도구에서 속성은 FLTL로 기술되는데 FLTL은 LTS 모델에서 액션을 가지고 속성을 표현하기에 적합하다. 우리는 기존 모델 체커들과의 실험을 통해서 개발된 도구의 성능을 비교분석한다. Since concurrent software is hard to debug, the verification of such systems inevitably needs automatic tools which support exhaustive searching. Bounded Model Checking(BMC) is one of them. Within a bound k, BMC exhaustively check some errors in execution traces of the given system. In this paper, we introduce the tool that performs BMC for LTS, modeling language for concurrent programs. In this tool, a property is described by a FLTL formula, which is suitable to present the property with actions in aLTS model. To experiment with existential model checkers and out tool, we compare and analysis the performance of the developed tool and others.
박사천 ( Sachoun Park ),권기현 ( Gihwon Kwon ) 한국정보처리학회 2008 한국정보처리학회 학술대회논문집 Vol.15 No.1
프로그램을 작성할 때 시스템의 성능을 높이기 위해서, 여러 개의 프로세스가 동시에 동작하고 상호작용하는 병행 프로그램을 사용한다. 병행 프로그램에서 프로세스들은 인터리빙 방식으로 동작하는 경우가 많다. 그런데 인터리빙을 잘 못 이해할 경우 프로그램에 오류가 생길 가능성이 높고 이러한 오류는 직관적으로 납득하지 못할 때도 많다. 본 논문에서는 인터리빙이 발생하는 최악의 경우를 소개하고 이를 SMV 와 Spin 그리고 LTS-BMC 로 정형 분석하는 방법에 대해서 설명한다. 또한 실험을 통해서 우리가 만든 LTS-BMC 도구가 병행 오류 검증에 효과적임을 알 수 있었다.
박사천 ( Sachoun Park ),이건수 ( Gunsoo Lee ),권기현 ( Gihwon Kwon ) 한국정보처리학회 2008 한국정보처리학회 학술대회논문집 Vol.15 No.1
본 논문은 게임 풀이를 통해서 모델 체킹 도구의 특징을 분석한다. 도망자-추적자 게임은 격자 모양의 미로에서 도망자가 추적자를 따돌리고 탈출하는 게임이다. 도망자가 격자 상에서 한 칸 움직일 때, 추적자는 일정한 패턴을 가지고 두 칸 움직인다. 이 문제를 SMV 와 SPIN 모델 체커로 모델링하고 검증하는 과정을 통해서 SMV 와 Spin 모델 체커의 특징을 분석한다. 실험을 통해서 우리는 최단 경로를 찾을 경우는 SMV 모델 체커를 사용해야 하고, 가능한 경로를 빨리 찾는 경우는 Spin 모델 체커가 더 적합함을 확인할 수 있었다.
박사천(Sachoun Park),이건수(Gunsoo Lee),권기현(Gihwon Kwon) 한국정보과학회 2008 한국정보과학회 학술발표논문집 Vol.35 No.1
SPIN은 소프트웨어 정확성 검사에 널리 사용되는 모델 검증 도구이다. 특히 C 코드로 작성된 소프트웨어를 효율적으로 검사하기 위해서 SPIN의 입력 언어인 Promela 모델에 C 코드를 끼워 넣는 기능이 버전 4.0 이상에서 지원되고 있다. 본 논문에서는 이러한 기능을 미로 게임 풀이에 적용하였다. 그 결과, Promela 모델만을 사용해서 풀이한 것보다도 모델에 C 코드를 끼워 풀이한 것이 메모리 사용 및 처리 시간에서 월등히 우수했다. 메모리와 시간과 같은 객관적인 성능 향상과 더불어서, 이러한 사례 연구는 모델 검증 도구 및 추상화 학습에도 유용함을 경험했다.
박사천(Sachoun Park),김태호(Taeho Kim),이화영(Hwayoung Lee) 한국정보과학회 2012 한국정보과학회 학술발표논문집 Vol.39 No.1B
최근 항공용 전자 시스템은 IMA (Integrated Modular Avionics) 방식으로 개발되고 있고 여기에는 실시간 운영체제의 표준인 ARINC 653이 적용되고 있다. ARINC 653은 시간적·공간적 파티셔닝을 제공함으로써 항공용 시스템의 안전성을 보장하며, OS 커널과 응용 소프트웨어 사이에 표준 API를 제공함으로써 두파트가 서로 독립적으로 개발될 수 있게 한다. 이러한 방식은 시스템의 이식성을 높일 수 있는데, 이를 보장하는 핵심 기법이 ARINC 653 설정이다. 본 논문에서는 산업현장에서 ARINC 653 설정을 쉽게 적용하여 응용 소프트웨어를 개발할 수 있는 도구를 소개한다.
이진 기수 조건에서 인접성 표현을 위한 최적화된 CNF 변환
박사천(Sachoun Park),권기현(Gihwon Kwon) 한국정보과학회 2008 정보과학회논문지 : 소프트웨어 및 응용 Vol.35 No.11
In some applications of software engineering such as the verification of software model or embedded program, SAT solver is used. To practical use a SAT solver, a problem is encoded to a CNF formula, but because the formula has lower expressiveness than software models or source codes, optimal CNF encoding is required. In this paper, we propose optimal encoding techniques for the problem of “Selecting adjacent k ≤ n among n objects.” Through experimental results we show the proposed constraint is efficient and correct to solve Japanese puzzle. As we know, this paper is the first study about CNF encoding for adjacency in BCC. 만족가능성 처리기는 모델 검증 및 임베디드 프로그램 검증과 같이 소프트웨어 공학의 여러 분야에서 활용되고 있다. 만족가능성 처리기를 활용하기 위해서는 주어진 문제를 처리기의 입력인 CNF 형식으로 변환해야 한다. 그러나 이 형식은 소스코드나 소프트웨어 모델보다 표현력이 낮기 때문에 최적화된 변환이 요구된다. 본 논문에서는 “n개에서 인접된 k ≤ n개 선택” 문제를 CNF형식으로 변환하는 최적화된 기법을 제시한다. 제안된 방법을 다양한 일본 퍼즐에 적용한 결과 우수한 성능이 입증되었다. 우리가 알고 있는 한, 인접성에 대한 최적화된 CNF 변환 연구는 거의 없다.
카운팅 문제에 대한 SAT, PB, SMT의 성능 분석
박호진 ( Hojin Park ),박사천 ( Sachoun Park ),권기현 ( Gihwon Kwon ) 한국정보처리학회 2008 한국정보처리학회 학술대회논문집 Vol.15 No.1
n개의 이진 변수 집합 중에 k개를 선택하는 카운팅 문제(Counting Problem)들은 여러 방법으로 풀이가 가능하다. 본 논문에서는 카운팅 문제를 풀기 위해 SAT, PB, SMT를 소개하고, 칸 칠하기(Fill-a-Pix) 퍼즐을 예로 들어 카운팅 문제의 인코딩 방법을 제시하고 처리 결과를 비교해 보았다. SAT이 상대적으로 인코딩은 가장 복잡했으나, 처리 시 가장 우수한 성능을 보였다. 따라서 본 논문은 카운팅 문제를 다룰 때에는 SAT이 가장 적합하다는 것을 제안한다.
손동환(Donghwan Son),박사천(Sachoun Park),김태호(Taeho Kim) 한국정보과학회 2012 한국정보과학회 학술발표논문집 Vol.39 No.1A
소셜 네트워크 서비스에 대한 관심이 높아지고 있으며 이의 하나로 인스턴트 메신저를 이용한 통합 커뮤니케이션 서비스의 필요성이 커지고 있다. 본 논문은 이러한 요구사항 중 그룹 내 회의를 진행하는 데 필요한 정보의 생성, 전송 및 저장을 위한 기능을 XMPP 기반 인스턴트 메신저 형태로 구현하였다.