| 1 |
1
컴퓨터 시스템에 의해 수행되는 정형 검증(Formal Verification)을 이용한 입출력 커널 구현의 강화 방법에 있어서, 입출력 커널의 강화를 위한 정형 검증을 수행하는 단계; 및 상기 정형 검증이 수행된 입출력 커널을 통해 신뢰실행환경에서 입출력 채널을 제공하는 단계 를 포함하는 강화 방법
|
| 2 |
2
제1항에 있어서, 상기 입출력 커널은 윔피 커널을 포함하고, 상기 정형 검증을 수행하는 단계는, 윔피 앱(App)에서 윔피 커널의 API가 호출될 때 자료구조 내에 구성된 엔트리들의 컨텐츠의 변경 여부를 통하여 윔피 커널의 구현을 증명하는 단계를 포함하고, 상기 자료구조는, 맵 형태로 구성된 디바이스디비(DeviceDB)를 포함하고, 상기 디바이스 디비의 엔트리들은 디바이스의 상태와 입출력 전송과 관련된 자료구조의 상태를 나타내는 것을 특징으로 하는 강화 방법
|
| 3 |
3
제1항에 있어서, 상기 입출력 커널은 윔피 커널을 포함하고, 상기 정형 검증을 수행하는 단계는, 입출력 장치로부터의 입력 데이터에 대한 비동기적인 DMA 트랜잭션에 제한적인 정책을 부과하는 단계를 포함하는 강화 방법
|
| 4 |
4
제3항에 있어서, 상기 정형 검증을 수행하는 단계는, 각각의 DMA 트랜잭션(Transaction)마다 DMA를 요청하는 API와 DMA 결과값을 반환하는 API를 포함하는 한 쌍의 API을 배치하고, 상기 DMA를 요청하는 API의 끝에서만 DMA 트랜잭션이 발생할 수 있도록 하여 스케줄러 활성화의 결과로서 나타나는 시스템의 상태가 하나만 나타날 수 있도록 제한하는 단계를 포함하는 강화 방법
|
| 5 |
5
제4항에 있어서, 상기 정형 검증을 수행하는 단계는, 상기 DMA 결과값을 반환하는 API에서 현재의 DMA 트랜잭션을 기준으로 이전의 DMA 트랜잭션이 성공적이었을 경우, 결과값을 반환하도록 하고, 스케줄러를 다시 비활성화시키고, USB의 비동기 리스트에 하나의 루트 타입 큐헤드(QueueHead)가 위치할 수 있도록 하고, 프레임 리스트(frame list) 내의 모든 프레임 리스트 링크 포인터(frame list link pointer)가 동일한 큐헤드를 가리키도록 하여 한 번에 하나의 DMA 트랜잭션만 발생하도록 제한하는 단계 를 포함하는 강화 방법
|
| 6 |
6
제1항에 있어서, 상기 정형 검증을 수행하는 단계는, 입출력 장치에서 입력 데이터가 전송되는 상황에 따라 결정적 함수와 비결정적 함수를 사용하는 단계 를 포함하는 강화 방법
|
| 7 |
7
제1항에 있어서, 상기 정형 검증을 수행하는 단계는, DMA 트랜잭션을 요청할 때 제한된 조건들을 모두 만족시키지 않을 경우, DMA 트랜잭션을 수행할 수 없도록 하고, DMA 트랜잭션이 수행될 때 트랜잭션의 내용을 변경할 API의 요청이 수행될 수 없도록 하는 단계를 포함하는 강화 방법
|
| 8 |
8
정형 검증(Formal Verification)을 이용한 입출력 커널 구현의 강화를 위한 컴퓨터 시스템에 있어서, 입출력 커널의 강화를 위한 정형 검증을 수행하는 정형 검증 수행부; 및 상기 정형 검증이 수행된 입출력 커널을 통해 신뢰실행환경에서 입출력 채널을 제공하는 입출력 채널 제공부 를 포함하는 컴퓨터 시스템
|
| 9 |
9
제8항에 있어서, 상기 입출력 커널은 윔피 커널을 포함하고, 상기 정형 검증 수행부는, 윔피 앱(App)에서 윔피 커널의 API가 호출될 때 자료구조 내에 구성된 엔트리들의 컨텐츠의 변경 여부를 통하여 윔피 커널의 구현을 증명하는 것을 포함하고, 상기 자료구조는, 맵 형태로 구성된 디바이스디비(DeviceDB)를 포함하고, 상기 디바이스 디비의 엔트리들은 디바이스의 상태와 입출력 전송과 관련된 자료구조의 상태를 나타내는 것을 특징으로 하는 컴퓨터 시스템
|
| 10 |
10
제8항에 있어서, 상기 입출력 커널은 윔피 커널을 포함하고, 상기 정형 검증 수행부는, 입출력 장치로부터의 입력 데이터에 대한 비동기적인 DMA 트랜잭션에 제한적인 정책을 부과하는 것을 특징으로 하는 컴퓨터 시스템
|
| 11 |
11
제10항에 있어서, 상기 정형 검증 수행부는, 각각의 DMA 트랜잭션(Transaction)마다 DMA를 요청하는 API와 DMA 결과값을 반환하는 API를 포함하는 한 쌍의 API을 배치하고, 상기 DMA를 요청하는 API의 끝에서만 DMA 트랜잭션이 발생할 수 있도록 하여 스케줄러 활성화의 결과로서 나타나는 시스템의 상태가 하나만 나타날 수 있도록 제한하는 것을 특징으로 하는 컴퓨터 시스템
|
| 12 |
12
제11항에 있어서, 상기 정형 검증 수행부는, 상기 DMA 결과값을 반환하는 API에서 현재의 DMA 트랜잭션을 기준으로 이전의 DMA 트랜잭션이 성공적이었을 경우, 결과값을 반환하도록 하고, 스케줄러를 다시 비활성화시키고, USB의 비동기 리스트에 하나의 루트 타입 큐헤드(QueueHead)가 위치할 수 있도록 하고, 프레임 리스트(frame list) 내의 모든 프레임 리스트 링크 포인터(frame list link pointer)가 동일한 큐헤드를 가리키도록 하여 한 번에 하나의 DMA 트랜잭션만 발생하도록 제한하는 것을 특징으로 하는 컴퓨터 시스템
|
| 13 |
13
제8항에 있어서, 상기 정형 검증 수행부는, 입출력 장치에서 입력 데이터가 전송되는 상황에 따라 결정적 함수와 비결정적 함수를 사용하는 것을 특징으로 하는 컴퓨터 시스템
|
| 14 |
14
제8항에 있어서, 상기 정형 검증 수행부는, DMA 트랜잭션을 요청할 때 제한된 조건들을 모두 만족시키지 않을 경우, DMA 트랜잭션을 수행할 수 없도록 하고, DMA 트랜잭션이 수행될 때 트랜잭션의 내용을 변경할 API의 요청이 수행될 수 없도록 하는 것을 특징으로 하는 컴퓨터 시스템
|
