혼합 도달성 분석을 이용한 상태 불변식의 단순화

권기현(Gihwon Kwon) 한국정보과학회 2003 정보과학회논문지 : 소프트웨어 및 응용 Vol.30 No.3·4

상태 불변식은 도달 가능한 모든 상태에서 만족되는 속성이다. 불변식은 복잡한 소프트웨어 시스템의 분석과 이해에 사용될 뿐만 아니라 안전성, 궁극성, 일관성등과 같은 시스템 검증에도 사용된다. 이와 같은 이유로 인해서, 유한 상태 기계 모델로부터 상태 불변식을 추출하는 연구가 활발히 진행되고 있다. 상태 불변식을 생성하는 기존 연구에서는 도달 가능한 상태가 모두 고려됐다. 따라서 생성된 상태 불변식은 길고 복잡해서, 사용자가 이해하기 어려웠다. 본 논문에서는 '어떻게 상태 불변식을 단순화 할 것인가?' 란 질문에 대한 답을 보인다. 상태 불변식의 복잡성은 고려되어진 상태의 크기에 강하게 좌우된다. 고려된 상태들이 작으면 작을수록, 상태 불변식의 길이는 짧다. 단순한 상태 불변식을 생성하기 위해서는, 전체 상태 공간보다는 관심 있는 특정 부분(즉 범위)에 집중해야 한다. 관심 있는 범위를 표현하기 위하여 본 논문에서는 CTL 논리를 사용한다. CTL로 범위가 표현되면, 혼합 도달성 분석을 이용하여 범위 내에 속하는 상태들을 찾는다. 명백히, 이 방법으로 계산된 상태 집합은 도달 가능한 모든 상태의 부분 집합이다. 따라서, 더 약하지만 더 이해력 있는 상태 불변식을 얻는다. State invariant is a property that holds in every reachable state. It can be used not only in understanding and analyzing complex software systems, but it can also be used for system verifications such as checking safety, liveness, and consistency. For these reasons, there are many vital researches for deriving state invariant from finite state machine models. In previous works every reachable state is to be considered to generate state invariant. Thus it is likely to be too complex for the user to understand. This paper seeks to answer the question 'how to simplify state invariant?' Since the complexity of state invariant is strongly dependent upon the size of states to be considered, so the smaller the set of states to be considered is, the shorter the length of state invariant is. For doing so, we let the user focus on some interested scopes rather than a whole state space in a model. Computation Tree Logic(CTL) is used to specify scopes in which he/she is interested. Given a scope in CTL, mixed reachability analysis is used to find out a set of states inside it. Obviously, a set of states calculated in this way is a subset of every reachable state. Therefore, we give a weaker, but comprehensible, state invariant.

SMV를 이용한 유한 상태 기계의 동치 검사

권기현(Gihwon Kwon),엄태호(Tae-Ho Eom) 한국정보과학회 2003 정보과학회논문지 : 소프트웨어 및 응용 Vol.30 No.7·8

본 연구에서는 유한 상태 기계들 간의 동치 여부를 검증하고자 한다. 즉 모든 입력에 대하여 유한 상태 기계의 반응이 항상 동일한지를 판정하고자 한다. 만약 두 개의 유한 상태 기계가 동치라고 판정된다면, 복잡한 유한 상태 기계는 단순한 기계로 대치될 수 있다. 또한 명세와 구현이 모두 유한 상태 기계로 표현된 경우, 동치 검사를 이용해서 구현이 명세를 만족하는지 결정할 수 있다. 본 논문에서는 이와 같은 유한 상태 기계의 동치 검사를 모델 검사 기법으로 다음과 같이 해결한다. 주어진 유한 상태 기계 M_A와 M_B를 조합하여 모델 M = M_A X M_B을 구축하고, 검사할 동치 조건을 시제 논리식 φ로 기술한다. 만일 모델이 시제 논리식을 만족한다면(M=φ) 두 기계는 동치이다. 그렇지 않다면 두 기계는 비동치이며 그 이유를 설명하는 반례를 제공한다. 전 과정이 자동화되었으며, 여러 개의 사례 연구에 적용한 결과 만족할 만한 결과를 얻었다. In this paper, we are interested in checking equivalence of FSMs(finite state machines). Two FSMs are equivalent if and only if their responses are always equal with each other with respect to the same external stimuli. Equivalence checking FSMs makes complicated FSM be substituted for simpler one, if they are equivalent. We can also determine the system satisfies the requirements, if they are all written in FSMs. In this paper, we regard equivalence checking problem as model checking one. For doing so, we construct the product model M = M_A X M_B from two FSMs M_A and M_B. And we also get the temporal logic formula φ from the equivalence checking definition. Then, we can check with model checker whether M satisfies φ, written M=φ. Two FSMs are equivalent, if M=φ. Otherwise, it is not equivalent. In that case, model checker generates counterexamples which explain why FSMs are not equivalent. In summary, we solve the equivalnce checking problem with model checking techniques. As a result of applying to several examples, we have many satisfiable results.

수도쿠 퍼즐을 통해서 살펴본 SAT에서 전처리 효과

권기현(Gihwon Kwon) 한국IT서비스학회 2008 한국IT서비스학회지 Vol.7 No.2

  The concept of preprocessing is widely used in various computer science area such as compiler and software engineering for the purpose of macro processing and optimization. In addition, preprocessing is also used in SAT solvers in order to eliminate redundant literals and clauses to speed up its solving time before searching the state space. However, there is an unexpected run-time error such as stack-overflow during this step, in case the size of a given set of clauses is huge which impedes SAT solvers. In this case, the preprocessing should be applied at the encoding time to optimize its size. In this paper this idea is applied to several Sudoku problems. As a result, significant improvements are obtained with respect to the number of variables and clauses as well as the solving time compared to the previous works.

SAT 처리기를 위한 수도쿠 퍼즐의 최적화된 인코딩

권기현(Gihwon Kwon) 한국정보과학회 2007 정보과학회논문지 : 소프트웨어 및 응용 Vol.34 No.7

SAT을 이용해서 수도쿠 퍼즐을 풀기 위해서는 수도쿠를 SAT 처리기의 표준 입력 언어인 CNF 논리식으로 인코딩 해야 한다. 기존에 제시된 인코딩 알고리즘으로 크기가 큰 수도쿠를 인코딩하면 현재 SAT 처리기의 처리 수준을 넘을 정도로 많은 논리식이 생성된다. 본 논문에서는 크기가 큰 수도쿠를 다루기 위해서 수도쿠의 고정 셀을 이용하여 최적화된 CNF 논리식을 생성하는 방법을 제시한다. 고정 셀에 배정된 숫자는 불변이기 때문에 이를 이용해서 일부 변수의 값을 인코딩 단계에서 미리 결정할 수 있고, 이들 변수의 값을 이용해서 SAT 처리에 영향을 주지 않는 절과 리터럴을 인코딩 단계에서 제거할 수 있다. 다양한 크기의 수도쿠 퍼즐에 적용한 결과 기존 인코딩 알고리즘에 비해서 우수한 성능을 보였다. Sudoku can be regarded as a SAT problem. Various encodings are known for encoding Sudoku as a Conjunctive Normal Form (CNF) formula, which is the standard input for most SAT solvers. Using these encodings for large Sudoku, however, generates too many clauses, which impede the performance of state-of-the-art SAT solvers. This paper presents an optimized CNF encodings of Sudoku to deal with large instances of the puzzle. We use fixed cells in Sudoku to remove redundant clauses during the encoding phase. This results in reducing the number of clauses and a significant speedup in the SAT solving time.

IEC 61508 안전 무결성 수준의 정량적 검증

권기현(Gihwon Kwon) 한국정보기술학회 2018 한국정보기술학회논문지 Vol.16 No.9

Safety function is a protection system of human life, economic loss and environmental damage against hazardous events which will cause an accident. Safety function performs its missions when it is demanded without failures if possible. IEC 61508 defines four discrete levels of SIL defining failure rates of safety function. When we develop safety function, SIL verification must be conducted. There has been a number of methods such as RBD and FTA used for quantitative SIL verification. This paper regards quantitative SIL verification as a probabilistic model checking problem. Thus, safety function is modelled as Continuous Time Markov Chain and properties specified as Continuous Stochastic Language. Then, our method is applied to a case study of Tank Overfill Protection in order to demonstrate the validity of our approach. As a result, we obtain the same result compared to formulas in IEC 61508. In addition, we can allow to analysis time-dependent behavior of safety function since Continuous Time Markov Chain is a dynamic model, not a static one like in RBD and FTA.

JADE를 이용한 합성된 오토마타의 시뮬레이션

권혁(Hyuck Kwon),권령구(Ryoungkwo Kwon),권기현(Gihwon Kwon) 한국정보과학회 2013 한국정보과학회 학술발표논문집 Vol.2013 No.11

오토마타 생성 시간 단축을 위한 분산 명세 합성

권혁(Hyuck Kwon),권령구(Ryoungkwo Kwon),권기현(Gihwon Kwon) 한국정보과학회 2014 한국정보과학회 학술발표논문집 Vol.2014 No.6

반응형 합성으로 합성된 유한 상태 전이 시스템의 추상화

권혁주(Hyeokju Kwon),권기현(Gihwon Kwon) 한국정보과학회 2016 한국정보과학회 학술발표논문집 Vol.2016 No.6

난청 환자들을 위한 소음 훈련 시스템 개발에 관한 연구

권혁 ( Hyuck Kwon ),이원기 ( Wonki Lee ),권기현 ( Gihwon Kwon ) 한국정보처리학회 2014 한국정보처리학회 학술대회논문집 Vol.21 No.1

본 연구에서는 난청 환자들을 위한 소음 훈련 소프트웨어 시스템 제안을 목표로 한다. 일반 병원에서도 난청 환자들을 위한 소음 훈련은 하지만, 이는 몇 가지 한계점들이 있다. 이러한 한계점들을 7.1 사운드 채널을 다루는 소프트웨어 시스템을 통해 극복하고자 하는 것이 본 연구의 목표이다.

[우수논문] GR(1) Synthesis를 이용한 퍼즐의 전략 찾기

권령구(Ryoungkwo Kwon),권기현(Gihwon Kwon) 한국정보과학회 2012 한국정보과학회 학술발표논문집 Vol.39 No.1B

본 논문에서 GR(1) Synthesis를 이용하여 퍼즐의 전략을 찾는 방법과 실험 결과를 기술한다. 먼저 GR(1) Synthesis와 승리 전략을 정형적으로 정의 하고, 퍼즐을 어떻게 형식화 할 것인지에 대하여 설명한다. 마지막으로 GR(1) Synthesis를 통해 획득한 승리 전략을 이용하여 GetOut 퍼즐을 해결하고 그 결과에 대하여 말한다.