http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
방기석(Ki-Seok Bang),공진산(Jin-San Kong) 한국정보과학회 2011 한국정보과학회 학술발표논문집 Vol.38 No.1D
고품질의 소프트웨어를 개발하기 위해 정확한 소스코드의 작성은 필수과정이다. 기능의 정확성 뿐만 아니라 근래에는 보안위협을 배제한 개발이 가장 중요한 품질의 척도가 되었다. 다양한 보안성 보장기법이 사용되고 도구가 개발되고 있지만 초보적 개발자들에게는 매우 어려운 과정이다. 본 연구에서는 소스코드 개발자에게 보안위협을 경고하고 그 대안을 제시할 수 있는 코드 작성기를 개발하고자 한다.
기상정보 활용을 통한 항공운항의 경영성과 제고 방안에 관한 연구
방기석 ( Ki Seok Bang ),김건하 ( Geon Ha Kim ) 한국생산성학회 2013 生産性論集 Vol.27 No.4
This study is intended to explore the effects of meteorological information on the aviation operation area. Most studies concerned with the valuation of meteorological information for aviation area have analyzed the flight cancelation or delay caused by meteorological factors with respect to the results rather than the internal processes. However, the aim of this paper is to deduce the causal relationship between the meteorological factors and the setbacks in the aviation operations through the proposed process analysis, which examines the errors during the decision-making process on the decision of flight cancelation or delay from the meteorological factors. The data related with the aviation operations of Gimpo airport and the meteorological data obtained in the domestic airport area during 2011 were adopted in this paper. We analyzed the data through three stages, i.e., basic statistical analysis, process analysis and evaluation of economic value. The result showed that the meteorological information could enhance the efficiency of the decision-making about the aviation operations.
방기석(Ki-Seok Bang),진현욱(Hyun-Wook Jin),최진영(Jin-Young Choi),유혁(Hyuck Yoo) 한국정보과학회 2003 정보과학회논문지 : 시스템 및 이론 Vol.30 No.1·2
본 논문에서는 모델 체킹을 시스템의 성능상의 효율성 분석에 적용하는 방법에 대해 논한다. 시뮬레이션이나 실험적인 측정을 통해 시스템의 성능저하를 찾는 것은 쉽지만, 성능을 저하시키는 요인을 분석해 내는 것은 사실상 매우 어렵다. 특히, 시스템 자체가 매우 복잡해지고, 주위 다른 시스템과의 상호 동작을 하게 되면 소스코드의 분석을 통한 오류 발견은 거의 불가능해진다. 이에 본 논문에서는 모델 체킹에 사용되는 시제논리를 통해 시스템의 자원 활용도를 명세하고, 이를 이용해서 모델 체킹을 수행함으로써 성능 저하를 발생시키는 요인을 찾아내는 방법에 대해 논한다. This paper addresses how model checking methods can be applied to utilization analysis of system. Measuring a system performance using simulation is an easy task but finding the bottleneck in a certain system is not an easy task. Especially, system is getting complicated and interacts with other systems, which makes the analysis very difficult. As an alternative approach, we show that can specify system utilization properties using temporal logic, and can find a reason of a system performance drop easily using model checking.
방기석(Ki-Seok Bang),김일곤(Il-Gon Kim),강인혜(Jin-Young Choi),강필용(In-Hye Kang),이완석(Pil-Yong Kang),최진영(Wan S. Yi) 한국정보과학회 2003 한국정보과학회 학술발표논문집 Vol.30 No.2Ⅰ
고등급의 침입 탐지 시스템 평가를 받기 위해서는 반드시 정형적인 방법론을 적용하여 시스템을 설계하고 검증해야 한다. 그러나 침입 탐지 시스템의 설계에 적합한 정형기법을 선정하기는 매우 어렵다. 본 논문에서는 정형 기법의 일종인 모델 체킹 방법론을 침입 탐지 메커니즘의 설계에 적용하는 방법을 제안하고, 고등급 침입 탐지 시스템의 개발에 사용할 수 있는 방향을 제시한다.
Bandera Toolset 을 이용한 객체지향형 소프트웨어 모델 체킹
방기석(Ki-Seok Bang),이주용(Joo-Yong Lee),최진영(Jin-Young Choi) 한국정보과학회 2001 한국정보과학회 학술발표논문집 Vol.28 No.2Ⅰ
객체지향형 소프트웨어가 개발되고 분산 시스템에 적용되면서 소프트웨어 시스템의 분석 및 안전성의 보장이 매우 어려워지고 있다. 정형 기법을 이용해서 소프트웨어 시스템의 안전성을 증명하는 연구가 진행되고 있지만 소스코드 레벨에서의 보장은 아직 어려운 상태이다. 본 연구에서는 이러한 소프트웨어 시스템의 소스코드 레벨에서의 안전성 보장을 위한 연구로 Bandera toolset 을 이용한 정형검증에 대해 논한다.
방기석 ( Ki-seok Bang ),공진산 ( Jin-san Kong ),강인혜 ( In-hye Kang ) 한국정보처리학회 2010 한국정보처리학회 학술대회논문집 Vol.17 No.2
정보시스템의 취약성을 사전에 예방하고 보안을 강화하기 위해 여러 가지 방안이 제시되고 있다. 본 연구에서는 소프트웨어의 소스코드 수준에서의 보안성을 확보하기 위해 소스코드 자체의 보안 위험성을 검사하는 도구를 제안한다. 개발자에 의해 무심코 사용되는 위험 함수들을 검출하고 그 대안을 제시하여 소프트웨어 내부에 잠재되는 보안 위협을 예방하는 도구를 개발하고자 한다.
방기석(Ki-Seok Bang),박명환(Myung-Whan Park),남원홍(Won-Hong Nam),최진영(Jin-Young Choi) 한국정보과학회 1999 한국정보과학회 학술발표논문집 Vol.26 No.2Ⅰ
Statechart는 다른 정형 명세와는 달리 그림으로 시스템을 명세하기 때문에 정형기법에 익숙하지 않은 사람도 이해할 수 있다. 또한 시스템의 동작을 보다 명확하고 가시적으로 시뮬레이션 할 수 있는 장점이 있다. 그러나 이 명세 방법은 시스템의 특성을 증명하는 정형 검증의 기능은 제공하고 있지 못한 것이 단점으로 지적되고 있다. 이러한 단점을 해결하기 위해 본 논문에서는 statechart로 기술된 명세를 정형 검증 언어인 SMV 및 PROMELA로 변환하여 검증하는 방법에 대해 논한다.
방기석(Ki-Seok Bang),류광열(Kwang-Yul Ryu),오정기(Jung-Ki Oh),최진영(Jin-Young Choi) 한국정보과학회 2000 한국정보과학회 학술발표논문집 Vol.27 No.1A
메시지 순서도(Message Sequence Chart, MSC)는 ITU-T에서 국제적인 표준으로 제안되어 주로 전기 통신 교환 시스템과 같은 실시간 시스템을 위한 통신 행위에 대한 개괄적인 표현 방법으로서 널리 사용되어지고 있으며 요구 명세, 인터페이스 명세, 시뮬레이션 및 검증을 위해 사용되어지고 있다. MSC의 장점이라면 표현된 시스템의 행위를 직관적으로 이해할 수 있게 해주는 그래픽 표현을 제공하는 것이다. 의미론 입장에서 보면 MSC는 프로세스 대수 ACP의 변형인 PA_ε에 의해 의미를 부여받고 있긴 하지만 이해하기가 난해한 것이 사실이다. 본 논문에서는 MSC의 동작적 의미를 분석하며 ACSR로 변환하여 그 의미를 보다 쉽게 파악하는 방법론에 대해 다룬다.