| 1 |
1
소프트웨어 프로그램을 검증하는 방법에 있어서,상기 검증할 소프트웨어 프로그램을 구성하는 다수의 함수들 중 대상 함수를 선정하는 단계;상기 대상 함수에 프로그램 합성 기법을 적용하여, 상기 대상 함수와 지정된 임계치 이상으로 유사한 결과를 출력하며 단순화된 합성 함수를 생성하는 단계; 및상기 대상 함수를 상기 합성 함수로 대체하고, 상기 대상 함수가 상기 합성 함수로 대체된 소프트웨어 프로그램을 검증하는 단계를 포함하는 방법
|
| 2 |
2
제 1 항에 있어서,상기 대상 함수를 선정하는 단계는사용자 선택, 랜덤 선택, 지정된 규칙, 및 검증 속성 중 적어도 하나에 기초하여 상기 대상 함수를 선정하는 단계를 포함하는 것을 특지응로 하는 방법
|
| 3 |
3
제 1 항에 있어서,상기 대상 함수를 선정하는 단계는배열 접근 계산식 및 배열 입력 범위 분석을 통해, 상기 대상 함수의 배열 요소들 중 상기 검증에 필요없는 배열 요소를 제외시키는 단계를 포함하는 것을 특징으로 하는 방법
|
| 4 |
4
제 1 항에 있어서,상기 합성 함수를 생성하는 단계는상기 프로그램 합성 기법을 이용하여, 플랫폼 종속적인 함수를 플랫폼 독립적인 함수로 변환하는 단계를 포함하는 것을 특징으로 하는 방법
|
| 5 |
5
제 1 항에 있어서,상기 합성 함수를 생성하는 단계는상기 대상 함수의 유효 입력 범위 내에서 랜덤하게 입력 값을 생성하는 단계;상기 생성된 입력 값에 기초하여 상기 대상 함수를 실행하는 단계;상기 대상 함수의 실행에 따른 입출력 예제를 생성하는 단계;상기 대상 함수의 실행 중 사용된 연산자, 인자, 및/또는 상수 값을 추출하는 단계;상기 추출된 연산자, 인자, 및/또는 상수 값을 이용하여 문법 제약을 생성하는 단계; 및상기 생성된 입출력 예제 및 상기 생성된 문법 제약에 기초하여 합성 스펙을 생성하고, 상기 생성된 합성 스펙에 기초하여 상기 대상 함수를 합성하여 상기 합성 함수를 생성하는 프로그램을 합성하는 단계를 포함하는 것을 특징으로하는 방법
|
| 6 |
6
제 1 항에 있어서,상기 검증하는 단계는상기 검증에 의해 생성된 반례를 분석하여 상기 검증 결과의 신뢰 여부를 확인하는 단계를 포함하는 것을 특징으로 하는 방법
|
| 7 |
7
제 6 항에 있어서,상기 검증 결과의 신뢰 여부를 확인하는 단계는상기 반례에 대하여, 상기 합성 함수의 출력 값이 상기 대상 함수의 출력 값과 일치하는지 여부를 확인하는 단계를 포함하는 것을 특징으로 하는 방법
|
| 8 |
8
소프트웨어 프로그램을 검증하는 장치에 있어서,상기 소프트웨어 프로그램을 검증하는 소프트웨어 검증 모듈을 저장하는 메모리; 및상기 소프트웨어 검증 모듈을 이용하여, 상기 소프트웨어 프로그램을 구성하는 다수의 함수들 중 대상 함수를 선정하고, 상기 대상 함수에 프로그램 합성 기법을 적용하여, 상기 대상 함수와 지정된 임계치 이상으로 유사한 결과를 출력하며 단순화된 합성 함수를 생성하고, 및 상기 대상 함수를 상기 합성 함수로 대체하고, 상기 대상 함수가 상기 합성 함수로 대체된 소프트웨어 프로그램을 검증하는 프로세서를 포함하는 것을 특징으로 하는 장치
|
| 9 |
9
제 8 항에 있어서,상기 프로세서는사용자 선택, 랜덤 선택, 지정된 규칙, 및 검증 속성 중 적어도 하나에 기초하여 상기 대상 함수를 선정하는 것을 특징으로 하는 장치
|
| 10 |
10
제 8 항에 있어서,상기 프로세서는배열 접근 계산식 및 배열 입력 범위 분석을 통해, 상기 대상 함수의 배열 요소들 중 상기 검증에 필요없는 배열 요소를 제외시킨 후, 상기 대상 함수에 상기 프로그램 합성 기법을 적용하는 것을 특징으로 하는 장치
|
| 11 |
11
제 8 항에 있어서,상기 프로세서는상기 프로그램 합성 기법을 이용하여, 플랫폼 종속적인 함수를 플랫폼 독립적인 함수로 변환하여 상기 합성 함수를 생성하는 것을 특징으로 하는 장치
|
| 12 |
12
제 8 항에 있어서,상기 프로세서는상기 대상 함수의 유효 입력 범위 내에서 랜덤하게 입력 값을 생성하고,상기 생성된 입력 값에 기초하여 상기 대상 함수를 실행하고,상기 대상 함수의 실행에 따른 입출력 예제를 생성하고,상기 대상 함수의 실행 중 사용된 연산자, 인자, 및/또는 상수 값을 추출하고,상기 추출된 연산자, 인자, 및/또는 상수 값을 이용하여 문법 제약을 생성하고, 및상기 생성된 입출력 예제 및 상기 생성된 문법 제약에 기초하여 합성 스펙을 생성하고, 상기 생성된 합성 스펙에 기초하여 상기 대상 함수를 합성하여 상기 합성 함수를 생성하는 것을 특징으로 하는 장치
|
| 13 |
13
제 8 항에 있어서,상기 프로세서는상기 검증에 의해 생성된 반례를 분석하여, 상기 검증 결과의 신뢰 여부를 확인하는 것을 특징으로 하는 장치
|
