| 1 |
1
응용 프로그램의 어플리케이션 모델 및 운영체제 모델을 통합하여 실행 시나리오 모델을 생성하는 단계;상기 실행 시나리오 모델에서 태스크 실행 순서 및 문장 블록을 도출하는 단계;상기 응용 프로그램의 실행에 따른 문맥 전환 위치를 주석첨가(annotate)하는 단계;상기 태스크 실행 순서 및 문장 블록과, 상기 문맥 전환 위치를 기초로 상기 응용 프로그램의 실행 가능한 경로를 검증하는 단계; 및상기 응용 프로그램의 실행 가능성을 확인하여 보고하는 단계를 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 2 |
2
제 1항에 있어서,상기 실행 시나리오 모델을 생성하는 단계는,모델 검증 도구 NuSMV를 이용하여 반례를 생성하는 단계를 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 3 |
3
제 2항에 있어서,상기 반례를 생성하는 단계는,상기 응용 프로그램의 태스크 스케줄링 정보 및 제어 흐름을 포함하는 상기 반례를 생성하는 단계를 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 4 |
4
제 2항에 있어서,상기 반례를 생성하는 단계는,API 호출 제약사항 준수 여부를 확인하여 상기 반례를 생성하는 단계를 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 5 |
5
제 1항에 있어서,상기 태스크 실행 순서 및 문장 블록을 도출하는 단계는,상기 태스크 실행 순서에 따라 각 태스크를 순서대로 호출하는 테스트 드라이버를 구현하는 단계를 더 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 6 |
6
제 1항에 있어서,상기 태스크 실행 순서 및 문장 블록을 도출하는 단계는,API 호출을 상기 문장 블록으로 도출하는 단계를 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 7 |
7
제 6항에 있어서,상기 문장 블록의 API 호출을 상기 응용 프로그램의 API 호출과 비교하는 단계를 더 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 8 |
8
제 1항에 있어서,상기 문맥 전환 위치를 주석첨가(annotate)하는 단계는,API 호출을 통해 태스크 생성 및 종료, 리소스 해제, 이벤트 대기 및 발생 시 문맥 전환이 발생하는 단계를 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 9 |
9
제 1항에 있어서,상기 응용 프로그램의 실행 중에 상기 문맥 전환 위치를 만나면 프로그램 카운터를 저장하고, 문맥 전환 후 재실행될 경우에 상기 저장된 프로그램 카운터를 이용하여 실행 위치로 복귀하는 단계를 더 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 10 |
10
제 1항에 있어서,상기 실행 가능한 경로를 검증하는 단계는,모델 검증 도구 CBMC를 이용하여 검증하는 단계를 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 11 |
11
제 10항에 있어서,상기 실행 가능한 경로를 검증하는 단계는,상기 응용 프로그램에서 반례와 동일한 순서로 API 호출을 수행하는 실행 경로의 존재 유무를 검증하는 단계를 포함하는, 응용 프로그램의 실행 가능성 확인 방법
|
| 12 |
12
응용 프로그램의 어플리케이션 모델 및 운영체제 모델을 통합하여 실행 시나리오 모델을 생성하는 모델 생성부;상기 실행 시나리오 모델에서 태스크 실행 순서를 도출하며, 상기 태스크 실행 순서에 따라 각 태스크를 순서대로 호출하는 테스트 드라이버를 생성하는 드라이버부;상기 실행 시나리오 모델에서 문장 블록을 도출하며, 상기 문장 블록의 API 호출을 상기 응용 프로그램의 API 호출과 비교하는 API 모니터를 생성하는 모니터링부;상기 응용 프로그램의 실행에 따른 문맥 전환 위치를 주석첨가(annotate)하여 주석첨가된 어플리케이션을 생성하는 주석첨가부;상기 테스트 드라이버, 상기 API 모니터, 상기 주석첨가된 어플리케이션을 이용하여 상기 응용 프로그램의 실행 가능한 경로를 검증하는 검증부; 및상기 응용 프로그램의 실행 가능성을 확인하여 보고하는 보고부를 포함하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 13 |
13
제 12항에 있어서,상기 모델 생성부는,모델 검증 도구 NuSMV를 이용하여 반례를 생성하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 14 |
14
제 13항에 있어서,상기 모델 생성부는,상기 응용 프로그램의 태스크 스케줄링 정보 및 제어 흐름을 포함하는 상기 반례를 생성하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 15 |
15
제 2항에 있어서,상기 모델 생성부는,API 호출 제약사항 준수 여부를 확인하여 상기 반례를 생성하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 16 |
16
제 12항에 있어서,상기 드라이버부는,반례에 나타난 태스크 실행 순서를 이용하여 상기 테스트 드라이버를 생성하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 17 |
17
제 12항에 있어서,상기 모니터링부는,상기 문장 블록의 API 호출을 상기 응용 프로그램의 API 호출과 비교하여 동일하지 않은 경우, 실행 가능한 경로의 검증 대상에서 제외하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 18 |
18
제 12항에 있어서,상기 주석첨가부는,API 호출을 통해 태스크 생성 및 종료, 리소스 해제, 이벤트 대기 및 발생 시 문맥 전환이 발생하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 19 |
19
제 12항에 있어서,상기 검증부는,모델 검증 도구 CBMC를 이용하여 검증하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 20 |
20
제 19항에 있어서,상기 검증부는,상기 응용 프로그램에서 반례와 동일한 순서로 API 호출을 수행하는 실행 경로의 존재 유무를 검증하는, 응용 프로그램의 실행 가능성 확인 장치
|
| 21 |
21
제 1항 내지 제 11항 중 어느 한 항의 방법을 구현하기 위한 프로그램이 기록된 컴퓨터로 판독 가능한 기록매체
|
