http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
SMV를 이용한 RACE 프로토콜의 정형 검증 및 테스팅
남원홍,최진영,한우종,Nam, Won-Hong,Choe, Jin-Yeong,Han, U-Jong 대한전자공학회 2002 電子工學會論文誌-CI (Computer and Information) Vol.39 No.3
본 논문은 심볼릭 모델 체커 SMV(Symbolic Model Verifier)를 이용하여, 한국전자통신연구원 (Electronics and Communications Research Institute)에서 개발한 캐쉬 일관성 프로토콜인 RACE(Remote Access Cache coherency Enforcement) 프로토콜의 몇 가지 특성(property)들을 검증함으로써, RACE 프로토콜이 중요 요구사항(requirement)들을 만족함을 보인다. 본 검증에서는 RACE 프로토콜의 모델을 SMV 입력 언어로 명세하며, 검증할 특성들을 CTL(Computational Tree Logic)을 이용하여 나타낸다. 본 검증을 통해서 RACE 프로토콜은 4개의 노드로 구성된 시스템에서 비정상적인 state/input 조합이 발생하지 않으며, liveness와 safety를 만족한다는 것을 검증하였다. 또한, 프로토콜 개발자들이 예상하지 못한 명세서 상의 모호성(ambiguity) 및 기아현상(starvation)을 발견하였으며, 본 검증 사례를 통하여 모델 체킹 기법이 하드웨어 프로토콜 검증에 효과적으로 이용될 수 있다는 것을 제안한다. 그리고, 검증시에 구현된 모델을 이용하여 시뮬레이션 및 테스팅에 유용하게 사용될 수 있는 테스트 케이스를 자동적으로 생성할 수 있는 새로운 방법을 제안한다. In this paper, we present our experiences in using symbolic model checker(SMV) to analyze a number of properties of RACE cache coherence protocol designed by ETRI(Electronics and Communications Research Institute) and to verify that RACE protocol satisfies important requirements. To investigate this, we specified the model of the RACE protocol as the input language of SMV and specified properties as a formula in temporal logic CTL. We successfully used the symbolic model checker to analyze a number of properties of RACE protocol. We verified that abnormal state/input combinations was not occurred and every possible request of processors was executed correctly We verified that RACE protocol satisfies liveness, safety and the property that any abnormal state/input combination was never occurred. Besides, We found some ambiguities of the specification and a case of starvation that the protocol designers could not expect before. By this verification experience, we show advantages of model checking method. And, we propose a new method to generate automatically test cases which are used in simulation and testing.
SMV를 이용한 RACE 프로토콜의 정형 검증 및 테스팅
南元洪,崔振榮,韓宇宗 대한전자공학회 2002 電子工學會論文誌-CI (Computer and Information) Vol.39 No.5
In this paper, we present our experiences in using symbolic model checker(SMV) to analyze a number of properties of RACE cache coherence protocol designed by ETRI(Electronics and Communications Research Institute) and to verify that RACE protocol satisfies important requirements. To investigate this, we specified the model of the RACE protocol as the input language of SMV and specified properties as a formula in temporal logic CTL. We successfully used the symbolic model checker to analyze a number of properties of RACE protocol. We verified that abnormal state/input combinations was not occurred and every possible request of processors was executed correctly We verified that RACE protocol satisfies liveness, safety and the property that any abnormal state/input combination was never occurred. Besides, We found some ambiguities of the specification and a case of starvation that the protocol designers could not expect before. By this verification experience, we show advantages of model checking method. And, we propose a new method to generate automatically test cases which are used in simulation and testing. 본 논문은 심볼릭 모델 체커 SMV(Symbolic Model Verifier)를 이용하여, 한국전자통신연구원(Electronics and Communications Research Institute)에서 개발한 캐쉬 일관성 프로토콜인 RACE(Remote Access Cache coherency Enforcement) 프로토콜의 몇 가지 특성(property)들을 검증함으로써, RACE 프로토콜이 중요 요구사항(requirement)들을 만족함을 보인다. 본 검증에서는 RACE 프로토콜의 모델을 SMV 입력 언어로 명세하며, 검증할 특성들을 CTL(Computational Tree Logic)을 이용하여 나타낸다. 본 검증을 통해서 RACE 프로토콜은 4개의 노드로 구성된 시스템에서 비정상적인 state/input 조합이 발생하지 않으며, liveness와 safety를 만족한다는 것을 검증하였다. 또한, 프로토콜 개발자들이 예상하지 못한 명세서 상의 모호성(ambiguity) 및 기아현상(starvation)을 발견하였으며, 본 검증 사례를 통하여 모델 체킹 기법이 하드웨어 프로토콜 검증에 효과적으로 이용될 수 있다는 것을 제안한다. 그리고, 검증 시에 구현된 모델을 이용하여 시뮬레이션 및 테스팅에 유용하게 사용될 수 있는 테스트 케이스를 자동적으로 생성할 수 있는 새로운 방법을 제안한다.
남원홍(Won-Hong Nam),최진영(Jin-Young Choi),한우종(Woo-Jong Han),심규현(Kyu-Hyun Shim) 한국정보과학회 1999 한국정보과학회 학술발표논문집 Vol.26 No.1A
본 논문은 심볼릭 모델 체커 중의 하나인 SMV(Symbolic Model Verifier)을 이용하여 캐쉬 일관성 프로토콜인 RACE(Remote Access Cache coherent Enforcement) 프로토콜의 몇 가지 특성(property)들을 검증한 사례를 제시한다. 이 검증을 통해서 RACE 프로토콜의 리모트 액세스에서 비정상적인 state/input 조합이 발생하지 않으며, 버스에서 발생할 수 있는 모든 요청(request)이 의도한 대로 처리된다는 것을 검증한다. 또한, 이러한 검증 사례를 통해서 체킹 검증 기법에 대한 장점들을 제시한다.
이더리움 스마트 컨트랙트 검증을 위한 ATL 모델 체킹
남원홍(Wonhong Nam),길현영(Hyunyoung Kil) 대한전기학회 2021 전기학회논문지 Vol.70 No.12
A blockchain is a growing list of cryptographically secured blocks to maintain shared data on decentralized systems, in order to archive transactions between untrusted participants. Smart contracts are computer programs that automatically execute legal events according to the terms of contracts. Although the Ethereum blockchain has been successfully applied to a number of interesting applications, there have been several events that subtle flaws in smart contracts induce a huge amount of financial loss such as the DAO attack. Accordingly, to analyze smart contracts, we propose a novel formal verification technique to employ ATL (Alternating-time Temporal Logic) model checking. Our methodology represents the interaction between users and smart contracts with a two-player game and verify game properties by using MCMAS that is an efficient ATL model checker.
남원홍(Won-Hong Nam),성창훈(Chang-Hun Sung),최진영(Jin-Young Choi),기안도(An-Do Ki),한우종(Woo-Jong Han) 한국정보과학회 2000 한국정보과학회 학술발표논문집 Vol.27 No.1A
본 연구는 심볼릭 모델 체커 중의 하나인 SMV(Symbolic Model Verifier)를 이용하여 한국전자통신연구원(ETRI)에서 개발한 CCA (Cache Coherent Agent) 보드를 위한 I-Link Bus(Inside Bus)의 몇 가지 특성(property)들을 검증하여 I-Link Bus의 요구사항(requirement)이 만족됨을 보인다. 이 검증에서는 I-Link Bus의 모델을 SMV 입력 언어로 명세하며, 검증할 특성들을 시제 논리(temporal logic)를 이용하여 나타낸다. 검증을 통해서 I-Link Bus와 PIF(Processor Interface), DC(Directory Controller), RC(Remote access cache Controller) 모듈들이 중재기 우선 순위, send 우선 순위, 중재 요청 신호의 관리, liveness 등의 특성들을 만족한다라는 것을 검증하였다.
QoS 기반 웹서비스 컴포지션을 위한 효율적인 리플래닝 기법
길현영,남원홍 대한전기학회 2020 전기학회논문지 Vol.69 No.11
A Web service is a service provided by software systems to support machine to machine inter-operations over Web. Given a set of Web services and a goal, the QoS-aware Web service composition problem constructs a composite Web service with the optimal accumulated QoS value, which satisfies the given goal specification. However, in the real world environment, frequent changes happen inherently ― for instance, temporary machine down, heavy system workload, and network failure. If the solution we have constructed is not valid anymore due to the changes, we have to solve a new problem again. Ordinary approaches to find a new solution from scratch may waste computation time, since they explore the whole searching space again. Hence, in this paper, we propose a novel replanning algorithm, which does not solve the new composition problem from scratch but explores only the changed space to identify the new optimal solution. In the experiment, our replanning algorithm can deal with the composition problem much faster than the original algorithm to solve from scratch.