http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
안소진(So Jin Ahn),심재환(Jae-Hwan Sim),남원홍(Wonhong Nam),최진영(Jin-Young Choi) 한국정보과학회 2011 한국정보과학회 학술발표논문집 Vol.38 No.1D
경합 상황, 교착 상태 등과 같은 동시 프로그램의 오류는 기존의 순차 프로그램에 적용되는 테스팅 방법으로는 탐지 및 재현이 힘들다. 하이젠버그라 불리는 이러한 오류는 프로그램의 안정성 및 신뢰성을 떨어뜨리는 원인이 될 수 있으므로 반드시 탐지하고 재현해야 한다. 본 논문은 SAT-solver와 경합 상태탐지를 위한 Happens-before 알고리즘을 사용하여 ANSI-C 프로그램 내 존재하는 이러한 오류를 탐지하고 재현할 수 있는 방법을 제안한다.
안소진(So Jin Ahn),황대연(Dae Yon Hwang),최진영(Jin-Young Choi) 한국정보과학회 2012 한국정보과학회 학술발표논문집 Vol.39 No.1A
정형기법은 소프트웨어 및 하드웨어 시스템의 요구사항을 모순, 모호함 없이 정확하게 명세하고 검증할 수 잇는 방법으로, 안전성이 중요한 소프트웨어에 많이 적용되어 반드시 보장되어야 할 속성을 소프트웨어가 만족하는지 확인하는데 사용되고 있다. 본 논문은 정형기법 커뮤니티에서 선정한 여러 도전 과제 중 하나인 인공 심장 박동기(pacemaker)를 실시간 속성을 표현할 수 있는 정형기법 도구인 UPPAAL을 사용하여 모델링하고 주요 속성을 검증하였다. 이를 통해 실시간 속성으로 인해 명세 및 검증하기 힘든 소프트웨어에 정형기법을 적용하여 안전성을 확학인할 수 있음을 보인다.
계층적 실시간 시스템 스케줄링 검증을 위한 정형적 프레임워크
안소진(So Jin Ahn),황대연(Dae Yon Hwang),최진영(Jin Young Choi) 한국정보과학회 2015 정보과학회 컴퓨팅의 실제 논문지 Vol.21 No.9
하드웨어가 많이 발전하면서 안전성 확보가 필요한 실시간 임베디드 시스템에도 가상화 기술이 적용되고 있는 추세다. 그러나 가상화 기술 적용 시, 스케줄러가 여럿 존재하게 되고, 이 스케줄러들 사이에 계층이 존재하게 되어 스케줄링 중 오류가 발생할 수 있는 단점이 있다. 임베디드 시스템의 제어 소프트웨어 같은 경우, 작은 문제로도 인명적, 재산적 피해가 클 수 있어 반드시 안전성 확보 여부를 검증해야 한다. 실시간 임베디드 시스템에 스케줄러가 계층적으로 존재하는 경우, 안전성 확보를 위해 반드시 스케줄링 가능성을 확인해야 한다. 본 논문은 여러 수준의 계층적 스케줄링 시스템을 정형기법(formal methods)을 사용하여 스케줄링 가능성을 확인할 수 있는 프레임워크를 소개한다. The use of Operating System(OS) virtualization is increasing as it provides many useful features such as efficient use of hardware(HW), easy system migration, and isolation between virtual spaces which prevents errors effecting each other. Recent development in HW has made it possible to use OS virtualization in embedded systems. However, implementing OS virtualization means that a multiple number of schedulers are layered in a system, rendering it difficult to analyze the schedulability of the system and errors are easily produced. Errors in safety critical embedded systems can cause serious damage to life and property; thus, the hierarchical schedulability must be verified. In this paper, we propose a framework which supports formal modeling and verification of hierarchical scheduling systems with UPPAAL.
정다혜(Da-Hye Jung),안소진(So-Jin Ahn),최진영(Jin-Young Choi) 한국정보과학회 2012 한국정보과학회 학술발표논문집 Vol.39 No.1B
소프트웨어 개발 시 코딩 규칙을 준수하면 소프트웨어에 잠재적으로 존재하는 프로그래밍 오류를 예방하는데 많은 도움이 된다. MISRA-C: 2004 는 고 신뢰성과 고품질이 요구되는 자동차, 우주항공, 통신, 등 제조분야에 대한 C언어 코딩 가이드 라인이다. 본 논문에서는 자동차와 우주항공같이 높은 안전성이 요구되는 원격 수소시스템을 타깃으로 하여 정적 분석한다. 그리고 분석 결과 발견된 오류 중 가장 빈번히 일어나는 오류에 대한 문제점을 분석하고 소프트웨어 품질 개선을 위하여 프로그래머들의 코딩 규칙 준수를 권장한다.
[소프트웨어 공학] 임베디드 S/W 개발 시프로그래밍 개선점 -MISRA-C를 중심으로
정다혜(Da-Hye Jung),안소진(So-Jin Ahn),최진영(Jin-Young Choi) 한국정보과학회 2013 정보과학회 컴퓨팅의 실제 논문지 Vol.19 No.3
소프트웨어 개발 시 코딩 규칙을 준수하면 소프트웨어에 잠재적으로 존재하는 프로그래밍 오류를 예방하는데 많은 도움이 된다. MISRA-C: 2004는 고 신뢰성과 고품질이 요구되는 자동차, 우주항공, 통신, 등 제조분야에 대한 C언어 코딩 규칙이다. 본 논문에서는 자동차와 우주항공같이 높은 안전성이 요구되는 원자력 발전소 활용 가능한 감시 시스템(가칭)을 타깃으로 하여 정적 분석한다. 그리고 분석 결과에서 발견된 오류 중 가장 빈번히 일어나는 오류에 대한 문제점을 분석하고 임베디드 소프트웨어 품질 개선을 위하여 각 임베디드 소프트웨어 분야별 코딩 규칙이 필요성을 제안하며 프로그래머들의 코딩 규칙 준수를 권장한다. When developing software, following coding standards prevents potential programming errors. MISRA-C: 2004 is a C language guideline for the automotive, aerospace, telecommunications and manufacturing industries which requires high reliability and quality. In this paper, a remote hydrogen system which requires high safety in fields like automotive and aerospace is being targeted for static analysis. Analysis of the target found frequently occurring errors. Code guidelines are suggested for each of the embedded software fields to improve quality and it is recommended that programmers continue to follow coding guidelines.
안드로이드의 LMK에 기반한 LRU 알고리즘 조정을 통한 특정어플리케이션의 실행 개시 속도 향상
류상선(Sangseon Ryu),안소진(So-Jin Ahn),최진영(Jin-Young Choi) 한국정보과학회 2014 정보과학회 컴퓨팅의 실제 논문지 Vol.20 No.5
본 논문에서는 안드로이드 운영체제를 이용하여 LMK에 기반한 LRU 알고리즘 조정을 통한 특정 어플리케이션(프로세스)의 실행 개시 속도 향상에 목표를 두었다. 실험을 통하여 LMK의 정상적 동작을 보장토록 시스템의 메모리 조건 충족 이후 LRU리스트를 인위적으로 조정 하게 되면, 특정한 지정 어플리케이션의 호출 성능을 최대 44%까지 향상시킬 수 있음을 확인하였다. 향후 전체적인 시스템 성능의 향상을 위하여 목표로 해야 할 어플리케이션들을 묶음으로 관리하는 방법의 연구가 추가로 필요하다. 또한 LMK에서 OOM Min Free를 6단계 슬롯 이상으로 세분화 하려는 추세에 맞추어 이에 따른 커널 및 프레임워크 관련부분들의 보완이 필요하다. In this paper we focus on the improvement of the launch speed of a specific Android application by the LRU algorithm adjustment based on the LMK. Our method considered the internal functionalities relationship between LRU list and Android activity stack. As the result of the experiments, we achieved up to 44 % of the progress with the modification of the LRU list after guaranteeing the normal operation requirements of the system memory. In the future, additional studies need to be considered for the management of the grouped applications for the purpose of the overall improvement of the system. According to the change of the LMK category, Linux kernel and android framework also should be revised.