| 1 |
1
삭제
|
| 2 |
2
차량 전장용 운영체제의 커널 코드(kernel code)로부터 안전성 특질과 연관된 코드를 추출하는 코드 추출부;추출된 상기 안전성 특질과 연관된 코드를 카테고리별로 재구성하여 복수 개의 모듈로 모듈화하는 모듈화부;모듈화된 복수 개의 모듈의 재구성된 코드를 모델 검증 언어를 기반으로 하는 정형 모델로 변환하는 정형 변환부; 및상기 차량 전장용 운영체제의 응용 프로그래밍 인터페이스로부터 범용 태스크 모델을 형성하여, 상기 정형 모델과 상기 범용 태스크 모델을 합성한 정형 검증 모델을 생성하는 범용 태스크 모델부를 포함하는 차량 전장용 운영체제의 정형 검증 장치
|
| 3 |
3
차량 전장용 운영체제의 커널 코드(kernel code)로부터 안전성 특질과 연관된 코드를 추출하는 코드 추출부;추출된 상기 안전성 특질과 연관된 코드를 카테고리별로 재구성하여 복수 개의 모듈로 모듈화하는 모듈화부; 및모듈화된 복수 개의 모듈의 재구성된 코드를 모델 검증 언어를 기반으로 하는 정형 모델로 변환하는 정형 변환부를 포함하며,상기 정형 변환부는,미리 결정된 모듈-프로메라(PROMELA) 대응규칙에 기초하여, 재구성된 코드를 상기 정형 모델로 변환함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 장치
|
| 4 |
4
제3 항에 있어서,상기 모듈-프로메라 대응규칙은,모듈화된 각 모듈, 각 모듈의 구성 함수, 및 공통 서비스 함수를 이와 대응하는 프로메라 구조로 번역하는 대응규칙인 것을 특징으로 하는 차량 전장용 운영체제의 정형 검증 장치
|
| 5 |
5
차량 전장용 운영체제의 커널 코드(kernel code)로부터 안전성 특질과 연관된 코드를 추출하는 코드 추출부;추출된 상기 안전성 특질과 연관된 코드를 카테고리별로 재구성하여 복수 개의 모듈로 모듈화하는 모듈화부; 및모듈화된 복수 개의 모듈의 재구성된 코드를 모델 검증 언어를 기반으로 하는 정형 모델로 변환하는 정형 변환부를 포함하며,상기 코드 추출부는,상기 커널 코드 중 안전성 특질에 기여하는 코어 함수를 식별하고, 식별된 상기 코어 함수의 코드를 상기 안전성 특질과 연관된 코드로 추출함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 장치
|
| 6 |
6
제5 항에 있어서,상기 모듈화부는,상기 코어 함수의 코드를 서비스 타입에 기반하여 복수 개의 그룹으로 분류함으로써, 상기 안전성 특질과 연관된 코드를 복수 개의 모듈로 모듈화함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 장치
|
| 7 |
7
제2 항 내지 제 6항 중 어느 한 항에 있어서,상기 코드 추출부는,각 응용 프로그래밍 인터페이스에 대해 호출 그래프(call graph)를 생성하고, 생성된 상기 호출 그래프의 코드 중에서 상기 안전성 특질과 연관된 코드를 추출함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 장치
|
| 8 |
8
삭제
|
| 9 |
9
차량 전장용 운영체제의 커널 코드(kernel code)로부터 안전성 특질과 연관된 코드를 추출하는 단계;추출된 상기 안전성 특질과 연관된 코드를 카테고리별로 재구성하여 복수 개의 모듈로 모듈화하는 단계;모듈화된 복수 개의 모듈의 재구성된 코드를 모델 검증 언어를 기반으로 하는 정형 모델로 변환하는 단계; 및상기 차량 전장용 운영체제의 응용 프로그래밍 인터페이스로부터 범용 태스크 모델을 형성하여, 상기 정형 모델과 상기 범용 태스크 모델을 합성한 정형 검증 모델을 생성하는 단계를 포함하는 차량 전장용 운영체제의 정형 검증 방법
|
| 10 |
10
제9 항에 있어서,상기 생성하는 단계는,상기 커널 코드에 대한 원시 변수 및 데이터의 타입을 프로메라(PROMELA) 타입으로 변환하는 단계를 포함함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 방법
|
| 11 |
11
차량 전장용 운영체제의 커널 코드(kernel code)로부터 안전성 특질과 연관된 코드를 추출하는 단계;추출된 상기 안전성 특질과 연관된 코드를 카테고리별로 재구성하여 복수 개의 모듈로 모듈화하는 단계; 및모듈화된 복수 개의 모듈의 재구성된 코드를 모델 검증 언어를 기반으로 하는 정형 모델로 변환하는 단계를 포함하며,상기 변환하는 단계는,미리 결정된 모듈-프로메라(PROMELA) 대응규칙에 기초하여 재구성된 코드를 상기 정형 모델로 변환함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 방법
|
| 12 |
12
차량 전장용 운영체제의 커널 코드(kernel code)로부터 안전성 특질과 연관된 코드를 추출하는 단계;추출된 상기 안전성 특질과 연관된 코드를 카테고리별로 재구성하여 복수 개의 모듈로 모듈화하는 단계; 및모듈화된 복수 개의 모듈의 재구성된 코드를 모델 검증 언어를 기반으로 하는 정형 모델로 변환하는 단계를 포함하며,상기 추출하는 단계는,상기 커널 코드 중 안전성 특질에 기여하는 코어 함수를 식별하는 단계를 포함하고, 식별된 상기 코어 함수의 코드를 상기 안전성 특질과 연관된 코드로 추출함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 방법
|
| 13 |
13
제12 항에 있어서,상기 추출하는 단계는,상기 커널 코드 중, 래퍼 함수(wrapper function)의 코드, 디버깅(debugging)을 위한 추적 함수(tracing function)의 코드, 하드웨어 의존(hardware dependent) 코드, 및 에뮬레이팅 함수(emulating function)의 코드를 제거함으로써, 상기 코어 함수를 식별하는 것을 특징으로 하는 차량 전장용 운영체제의 정형 검증 방법
|
| 14 |
14
제12 항에 있어서,상기 모듈화하는 단계는,상기 코어 함수의 코드를 서비스 타입에 기반하여 복수 개의 그룹으로 분류함으로써, 상기 안전성 특질과 연관된 코드를 복수 개의 모듈로 모듈화함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 방법
|
| 15 |
15
차량 전장용 운영체제의 커널 코드(kernel code)로부터 안전성 특질과 연관된 코드를 추출하는 단계;추출된 상기 안전성 특질과 연관된 코드를 카테고리별로 재구성하여 복수 개의 모듈로 모듈화하는 단계; 및모듈화된 복수 개의 모듈의 재구성된 코드를 모델 검증 언어를 기반으로 하는 정형 모델로 변환하는 단계를 포함하며,상기 차량 전장용 운영체제는 OSEK/VDX 표준에 기반하는 운영체제이고,상기 안전성 특질은 상기 OSEK/VDX 표준에 규정된 안전성 요구사항 또는 제한사항에 기반하여 결정되는 안전성 특징인 것을 특징으로 하는 차량 전장용 운영체제의 정형 검증 방법
|
| 16 |
16
제15 항에 있어서,상기 추출하는 단계는,각 응용 프로그래밍 인터페이스에 대해 호출 그래프(call graph)를 생성하고, 생성된 상기 호출 그래프의 코드 중에서 상기 안전성 특질과 연관된 코드를 추출함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 방법
|
| 17 |
17
제16 항에 있어서,상기 모듈화하는 단계는,상기 안전성 특질과 연관된 코드를 태스크 서비스(task service), 자원 관리(resource management), 이벤트 관리(event management), 스케쥴러(scheduler), 프로세스 서비스(process service), 및 공통 서비스 함수(common service functions)를 포함하는 카테고리별로 재구성함으로써 상기 복수 개의 모듈로 모듈화함을 특징으로 하는 차량 전장용 운영체제의 정형 검증 방법
|
| 18 |
18
제9 항 내지 제17 항 중 어느 한 항에 기재된 정형 검증 방법을 실행시키기 위한 프로그램을 기록한 컴퓨터로 읽을 수 있는 기록 매체
|
