모델 체킹을 이용한 도망자-추적자 게임 풀이

박사천,권기현 한국게임학회 2004 한국게임학회 논문지 Vol.4 No.2

우리는 도망자-추적자 게임 풀이에 관심이 많다. 도망자가 추적자를 피해 미로를 탈출하는 게임이다. 도망자가 추적자를 유인하기도 하고 벽을 이용해 교묘히 피하기도 한다. 경험에 의하면 수작업으로 풀기에는 매우 어려운 단계들도 있었다. 게임을 풀기 위한 방법으로 모델 체킹 기법을 사용하였다. 모델 체킹은 게임의 모든 상태 공간을 넓이 우선 방식으로 철저하게 탐색하기 때문에 게임을 풀 수 있는 가장 짧은 경로인 최적의 답을 구할 수 있다. 다행히 풀이 과정에서 상태 폭발 문제는 일어나지 않았고, 게임 풀이 결과를 임베디드 시스템인 레고 마인드스톰에 응용하였다. 도망자, 추적자에 해당하는 두 대의 에이전트를 만들어 게임을 구현하고 실험하여 풀이가 정확한 지를 실제 확인할 수 있었다. We have been interested in solving escapee-chaser game. In this game, with avoiding chaser, the escapee must escape from given male. The winning strategies of the escapee are driving the chaser to an intended place and closely evading from chaser by using some walls. According to our experience, some stages of the game are too difficult to solve manually. So we take the model checking method to get a solution of the game. Because the model checking with breadth fist search manner exhaustively searches the all state space of the game, the solution using model checking is best solution, shortest path. Fortunately, during the process of finding solution path, the state space explosion problem didn't occur, and the results of the game solving was applied to embedded system, Lego Mindstorm. Two agents, escapee and chaser, were implemented into robots and several experiments conformed the correctness of our solution.

효과적인 임베디드 소프트웨어 설계를 위한 제어흐름 모델의 자동 검증

박사천,권기현,하순회,Park, Sa-Choun,Kwon, Gi-Hwon,Ha, Soon-Hoi 한국정보처리학회 2005 정보처리학회논문지 A Vol.12 No.7

하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(Ptolemy extension as a Codesign Environment)에서는 데이터 흐름과 제어흐름을 모두 표현할 수 있다. PeaCE에서 제어 흐름을 표현하는 fFSM 명세를 정형 검증하기 위해 fFSM의 단계 의미를 정의하였다. 본 논문에서는 이전 연구에서 정의된 정형 의미를 바탕으로 개발한 자동 검증 도구를 소개한다. 이 도구는 내부 모델체커로 SMV를 사용하며 사용자는 직접 논리식을 기술하지 않고도 레이스 조건, 애매한 전이, 순환 전이 등의 주요한 버그들을 검증할 수 있다. Hardware and software codesign framework called PeaCE(Ptolemy extension as a Cod sign Environment) allows to express both data flow and control flow. To formally verify an fFSM specification which expresses control flow in PeaCE, the step semantics of the model was defined. In this paper, we introduce the automatic verification tool developed by formal semantics of previous work. This tool uses the SMV as inner model checker md, through our tool, users can formally verify some important bugs such as race condition, ambiguous transition, and circulartransition without directly writing logical formulae.

만족가능성 처리기를 이용한 이진 변수 서브시퀀스 추출

박사천,권기현,Park, Sa-Choun,Kwon, Gi-Hwon 한국정보처리학회 2008 정보처리학회논문지D Vol.15 No.6

Recently in the field of model checking, to overcome the state explosion problem, the method of using a SAT-solver is mainly researched. To use a SAT-solver, the system to be verified is translated into CNF and the Boolean cardinality constraint is widely used in translating the system into CNF. In BCC it is dealt with set of boolean variables, but there is no translating method of the sequence among Boolean variables. In this paper, we propose methods for translating the problem, which is extracting a subsequence with length k from a sequence of Boolean variables, into CNF formulas. Through experimental results, we show that our method is more efficient than using only BCC. 최근 정형 검증 분야에서 상태 폭발 문제를 극복하기 위해 만족가능성(Satisfiability) 처리기를 사용하는 방법이 많이 연구되고 있다. 만족가능성 처리기를 사용하려면 대상을 CNF 식으로 변환해야 하는데, 이진 기수 제약 조건은 시스템을 CNF 식으로 변환하기 위해 많이 사용되는 기법이다. 그러나 이진 기수 제약 조건은 이진 변수들의 집합을 다루기 때문에 이진 변수들의 순서 정보는 변환할 수 없었다. 본 논문에서는 이진 변수의 시퀀스에서 길이가 k인 서브시퀀스 추출 문제에 대한 CNF 변환 방법을 제안한다. 또한 실험을 통해 제안된 방법이 순서정보를 고려치 않고 적용한 변환 방법보다 훨씬 더 좋은 결과를 얻을 수 있었다.

효과적인 임베디드 소프트웨어 설계를 위한 제어흐름 모델의 자동 검증

박사천,권기현,하순회 한국정보처리학회 2005 정보처리학회논문지. 컴퓨터 및 통신시스템 Vol.12 No.7

Hardware and software codesign framework called PeaCE(Ptolemy extension as a Codesign Environment) allows to express both data flow and control flow. To formally verify an fFSM specification which expresses control flow in PeaCE, the step semantics of the model was defined. In this paper, we introduce the automatic verification tool developed by formal semantics of previous work. This tool uses the SMV as inner model checker and, through our tool, users can formally verify some important bugs such as race condition, ambiguous transition, and circulartransition without directly writing logical formulae. 하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(Ptolemy extension as a Codesign Environment)에서는 데이터 흐름과 제어 흐름을 모두 표현할 수 있다. PeaCE에서 제어 흐름을 표현하는 fFSM 명세를 정형 검증하기 위해 fFSM의 단계 의미를 정의하였다. 본 논문에서는 이전 연구에서 정의된 정형 의미를 바탕으로 개발한 자동 검증 도구를 소개한다. 이 도구는 내부 모델체커로 SMV를 사용하며 사용자는 직접 논리식을 기술하지 않고도 레이스 조건, 애매한 전이, 순환 전이 등의 주요한 버그들을 검증할 수 있다.

평탄화를 이용한 계층형 상태 기계의 단계 의미 정의

박사천,권기현,하순회 한국정보처리학회 2005 정보처리학회논문지D Vol.12 No.7

Hardware and software codesign framework called PeaCE(Ptolemy extension as a Codesign Environment) was developed. It allows to express both data flow and control flow which is described as fFSM which extends traditional finite state machine. While the fFSM model provides lots of syntactic constructs for describing control flow, it has a lack of their formality and then difficulties in verifying the specification. In order to define the formal semantics of the fFSM, in this paper, firstly the hierarchical structure in the model is flattened and then the step semantics is defined. As a result, some important bugs such as race condition, ambiguous transition, and circulartransition can be formally detected in the model. 하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(Ptolemy extension as a Codesign Environment)가 개발되었다. PeaCE 에서는 데이터 흐름과 제어 흐름을 모두 표현할 수 있는데, 제어 흐름은 상태 기계를 확장한 fFSM으로 나타낸다. fFSM은 계층형 상태 기계로서 제어 흐름을 표현하기 위해 많은 구문을 제공하지만, 모델에 대한 의미가 정의되어 있지 않아서 명세를 검증하는데 어려움이 많다. fFSM의 의미를 정의하기 위해서, 본 논문에서는 계층형 상태 기계를 먼저 평탄화한 후에 평탄화된 모델에 대해서 단계 의미를 정의하였다. 그 결과 레이스 조건, 애매한 전이, 순환 전이 등의 주요한 버그들을 정형적으로 검출할 수 있었다.

계층형 명세 언어의 정의 및 검사

박사천,권기현 한국정보과학회 프로그래밍언어연구회 2002 프로그래밍언어논문지 Vol.16 No.2

계층형 크립키 구조에서 HiCTL 해석

박사천,권기현 한국정보과학회 프로그래밍언어연구회 2001 프로그래밍언어논문지 Vol.15 No.2

정형논리를 이용한 모델링 및 분석

박사천,권기현 한국정보처리학회 2007 정보처리학회지 Vol.14 No.6

fFSM 모델의 정형 분석

박사천,권기현 한국정보과학회 프로그래밍언어연구회 2005 프로그래밍언어논문지 Vol.19 No.2

하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(ptolermy extension as a Codesign Environment)가 개발되었다. PeaCE에 서 fFSM(flexible Finite State Machine)은 제어흐름을 명세하도록 풍부한 구문을 제공하는 모델이지만, 정형 의미의 부재로 인해서 명세를 정형 분석하기가 어려웠다. 본 논문에서는 fFSM에 대한 정형 의미를 정의했고, 이를 통해서 정형 분석을 수행하는 프레임워크를 개발했다. 본 논문에서 개발된 프레임워크를 통해서 데드락, 레이스 조건(race condition), 애매한 전이(ambiguous transition), 순환 전이(circular transition)등과 같이 임베디드 소프트웨어에서 발생할 수 있는 중요한 버그들을 정형적으로 분석하는 방법을 보인다.

평탄화를 이용한 계층형 상태 기계의 단계 의미 정의

박사천,권기현,하순회,Park, Sa-Choun,Kwon, Gi-Hwon,Ha, Soon-Hoi 한국정보처리학회 2005 정보처리학회논문지D Vol.12 No.6

Hardware and software codesign framework called PeaCE(Ptolemy extension as a Codesign Environment) was developed. It allows to express both data flow and control flow which is described as fFSM which extends traditional finite state machine. While the fFSM model provides lots of syntactic constructs for describing control flow, it has a lack of their formality and then difficulties in verifying the specification. In order to define the formal semantics of the fFSM, in this paper, firstly the hierarchical structure in the model is flattened and then the step semantics is defined. As a result, some important bugs such as race condition, ambiguous transition, and circulartransition can be formally detected in the model. 하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(Ptolemy extension as a Codesign Environment)가 개발되었다. PeaCE 에서는 데이터 흐름과 제어 흐름을 모두 표현할 수 있는데, 제어 흐름은 상태 기계를 확장한 fFSM으로 나타낸다. fFSM은 계층형 상태 기계로서 제어흐름을 표현하기 위해 많은 구문을 제공하지만, 모델에 대한 의미가 정의되어 있지 않아서 명세를 검증하는데 어려움이 많다. fFSM의 의미를 정의하기 위해서, 본 논문에서는 계층형 상태 기계를 먼저 평탄화한 후에 평탄화된 모델에 대해서 단계 의미를 정의하였다. 그 결과 레이스 조건, 애매한 전이, 순환 전이 등의 주요한 버그들을 정형적으로 검출할 수 있었다.