게임 풀이를 위한 NuSMV의 효율적인 반례 생성

권기현,이태훈,Kwon, Gi-Hwon,Lee, Tae-Hoon 한국정보처리학회 2003 정보처리학회논문지D Vol.10 No.5

모델 검사는 모델이 속성을 만족하는지를 판정하기 위해서 모델의 상태 공간을 철저하게 조사한다. NuSMV는 모델 검사를 자동으로 수행하는 도구로서 본 논문에서는 이와 같은 NuSMV를 이용하여 푸쉬 푸쉬 게임을 해결한다. 모델이 속성을 만족하지 않는 경우 NuSMV는 그 이유를 설명하는 반례를 생성하게 되는데 NuSMV에 구현되어 있는 반례 생성 방식은 상태 공간을 2번 탐색하기 때문에 게임 풀이에 비효율적이다. 본 논문에서는 반례 생성시 상태 공간을 한 번만 탐색하도록 NuSMV를 재 구현 하였다. 그 결과 게임 풀이에 있어서 원래 NuSMV 보다 약 62%의 시간 절감과 11%의 공간 절감이 있었다. This paper solves Push-Push game with the model checker NuSMY which exhaustively explores all search space to determine whether a model satisfies a property. In case a model doesn't satisfy properties to be checked, NuSMV generates a counterexample which tells where this unsatisfaction occurs. However, the algorithm for generating counterexample in NuSMV traverses a search space twice so that it is inefficient for solving the game we consider here. To save the time to be required to complete the game, we revise the part of counterexample generation so that it traverses a search space once. As a result, we obtain 62% time improvement and 11% space improvement in solving the game with modified NuSMV.

트리의 노드 - 위치배정 알고리즘의 분석

권기현(Gi-Hwon Kwon) 한국정보과학회 1993 한국정보과학회 학술발표논문집 Vol.20 No.1

전산학 분야 뿐만 아니라 일반 분야에서 트리는 매우 광범위하게 사용된다. 트리를 잘 정돈된 형태로 그리는 것은 문제의 이해를 쉽게 해주며, 계층적인 관계를 분명히 나타낸다. 트리를 그리는데 있어서, 트리의 노드-위치배정이 가장 중요한 문제이다. 노드들은 서로 겹치지 않으면서, 가능한 한 적은 공간을 차지하도록, 그리고 노드들간에 균등한 간격을 유지하면서 미적으로 아름답게 배치되어야 한다. 이와 같은 조건을 만족하는 트리의 노드-위치배정을 위하여 제시된 6개의 알고리즘을 분석하였다. 또한 각 알고리즘을 프로그램하여 20개의 샘플 트리를 테스트하여본 경험을 기술한다. 알고리즘 1~5는 이진트리를 주로 다루고, 알고리즘 6은 자식 노드의 수에 제한을 두지 않는 일반 트리를 취급한다.

모델 체킹에서 상태 투영을 이용한 모델의 추상화

권기현 ( Gi Hwon Kwon ) 한국정보처리학회 2004 정보처리학회논문지D Vol.11 No.6

Although model checking has gained its popularity as one of the most effective approaches to the formal verification, it has to deal with the state explosion problem to be widely used in industry. In order to mitigate the problem, this paper proposes an abstraction technique to obtain a reduced model M' from a given original model M. Our technique identifies the set of necessary variables for model checking and projects the state space onto them. The abstract model M' is smaller in both size and behavior than the original model M, written M'≤M. Since the result of reachability analysis with M' is preserved in M, we can do reachability analysis with model checking using M' instead of M. The abstraction technique is applied to Push Push games, and two model checkers-Cadence SMV and NuSMV-are used to solve the games. As a result, most of unsolved games with the usual model checking are solved with the abstraction technique. In addition, abstraction shows that there is much of time and space improvement. With Cadence SMV, there is 87% time improvement and 79% space one. And there is 83% time improvement and 56% space one with NuSMV.

학습 알고리즘을 이용한 재사용 의사결정 지원

권기현(Gi Hwon Kwon),이경환(Kyung Whan Lee) 한국정보과학회 1994 정보과학회논문지 Vol.21 No.12

소프트웨어 재사용은 생산성과 품질을 높일수있는 전도유망한 방법이지만 실제 잘 활용되지 못하고 있다. 여기에는 여러가지 원인이 있겠지만 우리는 재사용 판정문제에 주목했다. 재사용 여부의 판정은 어려우나 중요하다. 지금까지 제시된 평가기법들은 대부분 메트릭을 기반으로 한다. 이러한 방식에서는 평가에 사용되는 메트릭과 구현사항이 강하게 결합되는 단점이 있다. 그 결과 메트릭의 변경 및 부품의 추가와 삭제가 어렵다. 본 연구에서는 학습 알고리즘을 이용하여 문제의 해결을 시도했다. 전문가의 판정지식을 학습한 후 학습결과에 따라서 검색된 부품의 재사용 여부를 판정한다. 제안한 기법은 판정지식과 구현사항이 분리되어있기 때문에 유연성과 확장성을 높인다. Software reuse is a promising approach to improve the productivity and quality of software. It also reduces the development time and the number of bugs. In spite of Its usefulness, software reuse isn't widely used. There are many reasons for not being widely used. Among these reasons, nontechnical issue such as the decision of reuse is important. Evaluation techniques proposed so far are based on metrics. This approachs would be tightly-coupled between metrics and implementation. In this paper, we tried to support the decision of reuse using learning algorithms which have been widely used in the area of artificial intelligence. Proposed techiniques give more flexibility and adpatability than metrics based approaches do.

원추리트리를 이용한 계층관계의 시각화

권기현(Gi Hwon Kwon) 한국정보과학회 1994 정보과학회논문지 Vol.21 No.10

트리는 폭넓게 사용되는 자료구조이다. 지금까지, 평면상에 트리를 그리는 알고리즘들이 많이 개발되었다. 그러나 트리의 깊이가 증가할수록 요구되는 폭이 지수승으로 증가하는 단점이 있다. 이러한 문제를 극복하기 위하여 3 차원상의 원추트리가 개발되었다. 그러나 원추들의 겹침현상이 발생되는 단점이 있다. 본 논문에서는, 원추들을 겹치지 않게 배치하는 기법과 원추의 반경을 최대화 하기 위한 트리 재구성기법등을 제시한다. 이러한 기법을 유닉스의 디렉토리 구조 시각화에 적용한다. Tree is a widely used data structure. So far, many algorithms were developed to draw a tree in 2-dimensional space. However, the required width increases exponentially corresponding to the depth of the tree. Cone tree in 3-dimensional space was also suggested to overcome this problem. But it does not avoid that cones are being overlapped. In this paper, we present some techniques to layout cones with nonoverlapping. And tree is restructed to maxmize a radius of cone as can as possible. With these techniques we visualize huge hierarchical relationships such as Unix directory structure.

소프트웨어 확장성에 관한 실험

권기현(Gi Hwon Kwon),배한수(Han Soo Bae),박희경(Hee Kyung Park),이경환(Kyung Hwan Lee) 한국정보과학회 1989 한국정보과학회 학술발표논문집 Vol.16 No.1

소프트웨어가 개발되어지고 난후 여러가지 변화 요인으로 인해 소프트웨어에 대한 유지보수 작업이 많이 행해지고 이러한 작업은 많은 인력과 비용을 소비하게 된다. 본 실험에서는 어떠한 형태로 소프트웨어가 설계되고 구현되어 질때 변화의 영향을 적게 받는지를 조사한다. 구조적 설계와 객체지향 설계, C 언어에 의한 구현과 C++ 언어에 의한 구현이 확장성의 관점에서 비교된다.

원시코드 재사용 지원 시스템에 관한 연구

권기현(Gi Hwon Kwon),박재흥(Jae Hung Park),이경환(Kyung Hawn Lee) 한국정보과학회 1987 한국정보과학회 학술발표논문집 Vol.14 No.1

최근 소프트웨어 수요와 개발비용이 급증하고 있다. 이러한 문제를 해결하기 위한 방법중 가장 두드러진 방법은 한번 쓰여진 소프트웨어를 다시 재사용하는 것이다. 소프트웨어를 재사용함으로서 개발 기간의 단축, 프로그래머의 노력 감소, 신뢰성 향상 등의 여러 잇점을 얻을 수 있다. 본 논문에서는 C 언어로 소프트웨어를 개발하는 경우 원시코드를 재사용할 수 있도록 지원해주기 위한 원시코드 재사용 지원 시스템을 구현하였다.

VDM을 사용한 정형적 명세의 동작 모형 구축

권기현(Gi Hwon Kwon),이관석(Kwan Suk Lee) 한국정보과학회 1995 정보과학회논문지(B) Vol.22 No.9

모델 기반 명세인 VDM 은 집합, 시퀀스, 맵 그리고 복합객체의 네가지 추상 자료형으로 시스템 상태를 모델한다. VDM 으로 작성된 정형적 명세의 문제점은 읽기 어렵고 난해하다. 명세가 사용자, 명세자, 그리고 설계자간의 계약서로 활용되기 위해서 이러한 문제점들이 해결되어야 한다. 본 논문에서는 정형적 명세의 동작모형 구축방법을 제시한다. 동작모형은 최종 프로그램의 모형이면서 실행가능하며, 기존의 프로토타이핑 방식의 실행과는 달리 애니메이션 방식으로 실행된다. 동작모형 구축을 위하여 Enact 라는 모델링 언어를 사용하였으며,VDM 의 자료형에 대응하는 클래스를 설계하였다. 동작모형을 이용한 정형적 명세의 실행은 상태의 변화 과정을 명확히 보여주며, 최종 시스템의 윤곽을 조기에 보여준다. 또한 추상 명세를 구체 명세로 정제할때 준수해야할 증명의무를 도와준다. VDM have four abstract data types to model the system state: set. sequence, map. and composite objects. It is usually difficult to read and understand formal specification. In this paper. we present the method of constructing the working model for formal specification with VDM. The working model which is executable reflects a final product and allows formal specification to be animated rather than prototyped. It shows clearly the state transition. gives a good indication of what the final product will be like, and helps the proof obligations discharged with refinement. It is constructed by the modelling language Enact.

시각 질의에서 발생하는 애매한 질의의 해결 방법

권기현(Gi-Hwon Kwon),정관희(Kwan-Hee Jung),이경환(Kyung-Hwan Lee) 한국정보과학회 1991 한국정보과학회 학술발표논문집 Vol.18 No.1

초보자들의 질의 표현을 도와주기 위한 여러가지 유형의 인터페이스 시스템들이 개발되고 있다. 이들 중 아이콘을 사용하여 질의를 표현하는 방법이 많이 사용되고 있다. 검색하고자 하는 정보에 해당하는 아이콘을 선택하여 공간상에 배열해 나감으로서 찾고자하는 정보에 대한 질의를 표현한다. 그러나 아이콘의 배열에 의한 질의는 정보의 부족으로 애매한 질의를 형성하게 된다. 이에 본 논문에서는 애매한 질의를 받아들여 완전한 질의로 변형하는 알고리즘 FT(Fuzzy query To Complete query)을 제안하여 자동차 데이타 베이스에 적용해 보았다.

재귀를 이용한 트리 구조의 시각화 및 적용

권기현(Gi Hwon Kwon) 한국정보과학회 1994 한국정보과학회 학술발표논문집 Vol.21 No.1

컴퓨터 그래픽을 이용하여 트리를 시각화하는 것은 흥미있는 일이다. 왜냐하면, 트리는 실세계의 문제 모델링에 많이 이용되며 또한 많은 알고리즘들이 트리를 기반으로 하기 때문이다. 트리를 시각화함으로서 문제의 직관적인 이해향상 및 계층관계를 쉽게 파악할 수 있다. 트리 시각화를 위하여 제시된 기존 알고리즘의 단점들은 다음과 같다: 복잡한 구조 표현의 부적절, 스크롤링의 부담, 동적인 조정의 어려움 등, 실세계의 문제는 매우 복잡한 구조로 구성되어 있다. 복잡한 구조를 효율적으로 시각화하기 위하여 재귀를 이용하였다. 재귀의 자기유사성 특징을 이용하여 서로 중첩되지 않도록 노드의 위치를 배정한다. 제시된 방식을 히프정렬 알고리즘의 애니메이션 및 유닉스 디렉토리 브로우져에 적용하여본 결과 복잡한 구조를 효율적으로 그렸다.