http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
차량 전장용 운영체제의 주기적 태스크 검증을 지원하는 테스트 케이스 생성기
최우용 ( Wooyong Choi ),김동우 ( Dongwoo Kim ),최윤자 ( Yunja Choi ) 한국정보처리학회 2017 한국정보처리학회 학술대회논문집 Vol.24 No.1
안전 필수 시스템(Safety-critical system) 중 하나인 차량 전장용 운영체제의 엄밀한 검증을 위하여 모델 기반 테스트 생성기법들이 연구되어 왔다. 그러나 기존의 연구들은 이러한 차량 전장용 운영체제에서 빈번히 사용되는 주기적인 동작을 요하는 작업들에 대한 테스트 생성 문제를 해결하지 못하였다. 본 연구에서는 주기적 태스크의 검증을 지원하지 않았던 기존의 테스트 케이스 생성기에 알람 모델을 추가하여 보완하였다. 이를 통해 차량 전장용 운영체제의 검증에 있어서 주기적 태스크를 포함한 다양한 테스트 케이스를 생성할 수 있었고 차량 전장용 운영체제의 보다 엄밀한 검증이 가능해졌다.
효과적인 멀티태스크 프로그램 검증을 위한 KLEE와 CBMC의 오경보 식별 성능 비교
김동우(Dongwoo Kim),최윤자(Yunja Choi) 한국정보과학회 2021 정보과학회논문지 Vol.48 No.2
OiL-CEGAR[1]는 정확한 검증을 위해 정형 운영체제 모델을 사용하고 프로그램을 정형모델로 변환해 검증함으로써 운영체제와 프로그램 모두를 고려하여 검증하였다. 하지만, 프로그램의 추상화로 인한 오경보가 보고될 수 있었으며 이를 제거하기 위한 실행 가능성 검사는 고비용이 요구되어 검증 성능개선을 위해서는 오경보 식별 성능의 개선이 꼭 필요하다. 본 연구에서는 실행 가능성 검사를 위한 두 가지 방법을 소개하고 비교하였다. 첫 번째 방법은 CBMC를 이용하며 전체 프로그램의 수식을 만들고 반례에 나타난 모든 블록의 도달 가능성을 한 번에 확인한다. 두 번째 방법은 KLEE를 이용하며 이진 탐색 기반 실행 가능성 검사를 통해 반례의 실행 불가능한 블록을 식별한다. 실험에서는 차량전장용 창문 제어프로그램의 검증에 각 실행 가능성 검사를 적용한 결과 KLEE를 이용했을 때 실행 가능성 검사 시간을 1/2000 수준으로 낮추었으며 전체 검증 시간을 11.78% 단축할 수 있었다. OiL-CEGAR[1] verifies the composition of a formal OS model and an abstracted application program for accurate verification. Due to the use of the abstract program, however false-alarms can be reported and executability checking for identifying false-alarms requires a high cost. Therefore, efficient executability checking is essential to improve verification performance. To find an effective executability checking method, this study introduces and compares two different techniques that perform executability checking. The first one collects the Boolean formula for the entire program and checks the reachability of all the program blocks in the counterexample by using CBMC. While the second one uses KLEE and identifies non-executable blocks in the counterexample through the binary search-based executability checking. The suggested executability checking methods are applied to a window controller program from the automotive domain. Results show that executability checking using KLEE takes only 1/2000 time compared to that of CBMC and reduces 11.78% of OiL-CEGAR verification costs.
프로그램 합성 기법을 이용한 임베디드 소프트웨어의 모델 체킹 효율성 향상을 위한 사례 연구
김요엘(Yoel Kim),최윤자(Yunja Choi) 한국정보과학회 2021 한국정보과학회 학술발표논문집 Vol.2021 No.12
C언어로 작성된 임베디드 소프트웨어를 엄밀히 검증하기 위해 모델 검증기 CBMC을 사용할 수 있으나, 소프트웨어가 복잡할수록 검증 효율성이 크게 감소하는 문제가 있었다. 이를 해결하기 위한 방법으로 프로그램 합성 기법을 사용해 검증 대상 함수를 좀 더 단순한 형태의 동일 행위를 갖는 함수로 합성함으로써 검증 시간을 단축하려는 시도가 있었으나, 합성 기법은 큰 사이즈의 배열을 가진 함수의 합성 정확도가 낮아 실제로 검증에 적용하기 어려웠다. 이를 해결하기 위해 본 연구에서는 배열 인덱스 계산식 및 배열 입력 범위 분석을 통해 검증에 필요 없는 입력 범위를 제거하여 합성 난이도를 줄였고, 기존 보다 더 정확하면서 간결한 함수를 합성할 수 있었다. 이를 Object Follower 예제에 적용한 결과 CBMC 실행 시간이 10배 이상 단축되었으며, 검증 결과의 신뢰성을 높일 수 있었다.
소프트웨어 공학 : 온라인 게임 서버의 파티 시스템 검증을 위한 스핀 모델 체커 적용에 관한 연구
김광훈 ( Goanghun Kim ),최윤자 ( Yunja Choi ) 한국정보처리학회 2015 정보처리학회논문지. 소프트웨어 및 데이터 공학 Vol.4 No.11
모델 체킹 방법은 가능한 모든 경우를 자동으로 확인할 수 있으며, 코드가 구현되기 이전의 명세서나 디자인의 검증에도 적용할 수 있어 고위험 시스템의 검증에 활발히 적용되어왔다. 그러나 이러한 엄밀한 검증기법에 대한 일반적인 이해 부족과 테스팅에 비해 높은 검증 비용으로 인하여, 일반적인 소프트웨어들은 여전히 인력에 의한 테스팅과 같은 기초적인 방법에 의존하여 검증이 수행되고 있다. 본 논문에서는 그 대표적인 예인 온라인 게임 서버를 대상으로, SPIN 모델 체커(SPIN model checker)를 이용한 자동화 검증 방법을 적용하는 실험적인 연구를 수행하여 검증 비용 대비 효과에 근거한 적용성을 판단하였다. 연구 결과, 5~7GB 이내의 메모리와 10분 이내의 시간 내에서 온라인 게임 서버 파티 시스템의 주요 특성들을 검증할 수 있음을 보였고, 이 과정에서 기존에 파악하지 못한 오류도 검출하였다. 이로부터 인력에 의한 테스팅에 비해 납득할만한 수준의 검증 비용으로 엄밀하고 효과적인 검증이 가능하다는 결론을 도출할 수 있었다. Model checking method is able to check all possible cases automatically and is applicable to specifications or design before actual implementation so that some critical systems have adopted this method actively. However, the current practice of software verification is largely dependant on basic methods such as manual testing because of lack of understanding about this rigorous method and high verification cost. In this paper we conducted an experimental research for the automated verification using the SPIN model checker on an online-game server to study the applicability of the technique in this domain. The results show that we could verify major features of the online-game server party system with 5~7 GB memory and within 10 minutes execution time, and also found a hidden system error that passed existing testing process. This result shows the possibility of rigorous and effective verification with reasonable cost in comparison to manual testing.
박민규 ( Min-gyu Park ),최윤자 ( Yunja Choi ),김진삼 ( Jinsam Kim ) 한국정보처리학회 2010 한국정보처리학회 학술대회논문집 Vol.17 No.2
안전중요 소프트웨어 코드의 검증은 1%의 잠재적 가능성을 가진 오류조차 허용하지 않는 철저한 검증방식을 요구한다. 이러한 요구에 부응하여 최근 수학적 모델을 사용한 정형검증 기법이 코드검증에 활발하게 적용되고 있으나, 코드의 복잡도와 크기의 증가에 따른 검증비용의 기하급수적 증가가 해결과제로 부각되어왔다. 본 연구에서는 검증하고자 하는 특성을 중심으로 검증대상 코드를 추출, 정형검증의 대상을 자동으로 축소하는 코드추출기를 개발하였다. 개발된 코드추출기는 자동차 전장용 운영체제의 검증에 보조적으로 활용되어 검증비용을 90% 이상 절감하고 검증 사용성을 높이는데 기여하였다.