| 1 |
1
스케줄러가 계층적으로 존재하는 실시간 시스템에 있어서,상기 시스템의 요구 사항을 입력받는 입력부;상기 요구 사항 수신하고, 타임드 오토마타(Timed Automata) 기반의 정형 기법을 이용하여 상기 시스템에서 문제가 되는 부분을 직관적으로 확인할 수 있는 정형 명세를 생성하는 정형 명세 생성부; 및상기 정형 명세를 모델 검사(Model Checking) 도구를 이용하여 검증을 수행하는 정형 검증 수행부;를 포함하되,상기 정형 명세 생성부는 상기 시스템의 최상위 스케줄러의 모델을 명세하는 최상위 스케줄러 모델 생성부, 상기 시스템의 적어도 하나 이상의 하위 스케줄러 모델을 명세하는 하위 스케줄러 모델 생성부, 및 상기 시스템의 적어도 하나 이상의 태스크를 명세하는 태스크 모델 생성부를 포함하고,상기 요구 사항은상기 최상위 스케줄러의 스케줄링 정책과 상기 최상위 스케줄러의 워크로드 정보를 포함하는 최상위 스케줄러 요구 사항,상기 하위 스케줄러의 스케줄링 정책과 상기 하위 스케줄러의 워크로드 정보를 포함하는 제1 하위 스케줄러 요구 사항, 상기 하위 스케줄러의 주기, 상기 하위 스케줄러의 주기 중 필요한 실행 시간, 및 상기 하위 스케줄러의 우선순위를 포함하는 제2 하위 스케줄러 요구 사항, 및상기 태스크의 주기, 상기 태스크의 데드라인, 상기 태스크의 시작 오프셋, 상기 태스크의 우선순위, 및 의존성 정보를 포함하는 태스크 요구 사항을 포함하며, 상기 하위 스케줄러는 다른 하위 스케줄러 또는 상기 최상위 스케줄러의 하위 계층의 스케줄러이며, 상기 하위 스케줄러가 실행 시간을 모두 소모하지 않고 주기가 종료한 경우에도 상기 하위 스케줄러에 스케줄링을 요청하는 워크로드가 존재하지 않는다면 스케줄링 가능한 것으로 판단하고,상기 의존성 정보는 상기 태스크가 의존하는 의존 태스크를 나타내며,상기 의존 태스크의 실행이 완료되지 않은 경우 상기 태스크에 대한 스케줄링은 요청되지 않는,정형 검증 장치
|
| 2 |
2
삭제
|
| 3 |
3
제1항에 있어서, 상기 모델 검사(Model Checking) 도구는 UPPAAL인 것을 특징으로 하는,정형 검증 장치
|
| 4 |
4
제1항에 있어서,상기 정형 검증 수행부는 TCTL(timed CTL)을 이용하여 모델 검사를 수행하기 위한 검증 속성을 명세하는 것을 특징으로 하는, 정형 검증 장치
|
| 5 |
5
입력부, 정형 명세 생성부, 및 정형 검증 수행부를 포함하는 정형 검증 장치를 이용하여 스케줄러가 계층적으로 존재하는 실시간 시스템의 정형 검증을 수행하는 방법에 있어서,상기 입력부가 상기 시스템의 요구 사항을 입력받는 요구 사항 입력 단계;상기 정형 명세 생성부가 상기 요구 사항 수신하고, 타임드 오토마타(Timed Automata) 기반의 정형 기법을 이용하여 상기 시스템에서 문제가 되는 부분을 직관적으로 확인할 수 있는 정형 명세를 생성하는 정형 명세 생성 단계; 및상기 정형 검증 수행부가 상기 정형 명세를 모델 검사(Model Checking) 도구를 이용하여 검증을 수행하는 정형 검증 수행 단계;를 포함하되,상기 정형 명세 생성 단계는 상기 시스템의 최상위 스케줄러의 모델을 명세하는 최상위 스케줄러 모델 생성 과정, 상기 시스템의 적어도 하나 이상의 하위 스케줄러 모델을 명세하는 하위 스케줄러 모델 생성 과정, 및 상기 시스템의 적어도 하나 이상의 태스크를 명세하는 태스크 모델 생성 과정을 포함하고,상기 요구 사항은상기 최상위 스케줄러의 스케줄링 정책과 상기 최상위 스케줄러의 워크로드 정보를 포함하는 최상위 스케줄러 요구 사항,상기 하위 스케줄러의 스케줄링 정책과 상기 하위 스케줄러의 워크로드 정보를 포함하는 제1 하위 스케줄러 요구 사항,상기 하위 스케줄러의 주기, 상기 하위 스케줄러의 주기 중 필요한 실행 시간, 및 상기 하위 스케줄러의 우선순위를 포함하는 제2 하위 스케줄러 요구 사항, 및상기 태스크의 주기, 상기 태스크의 데드라인, 상기 태스크의 시작 오프셋, 상기 태스크의 우선순위, 및 의존성 정보를 포함하는 태스크 요구 사항을 포함하며,상기 하위 스케줄러는 다른 하위 스케줄러 또는 상기 최상위 스케줄러의 하위 계층의 스케줄러이며,상기 하위 스케줄러가 실행 시간을 모두 소모하지 않고 주기가 종료한 경우에도 상기 하위 스케줄러에 스케줄링을 요청하는 워크로드가 존재하지 않는다면 스케줄링 가능한 것으로 판단하고,상기 의존성 정보는 상기 태스크가 의존하는 의존 태스크를 나타내며,상기 의존 태스크의 실행이 완료되지 않은 경우 상기 태스크에 대한 스케줄링은 요청되지 않는,정형 검증 방법
|
| 6 |
6
삭제
|
| 7 |
7
제5항에 있어서, 상기 모델 검사(Model Checking) 도구는 UPPAAL인 것을 특징으로 하는,정형 검증 방법
|
| 8 |
8
제5항에 있어서, 상기 정형 검증 수행 단계는 TCTL(timed CTL)을 이용하여 모델 검사를 수행하기 위한 검증 속성을 명세하는 단계를 더 포함하는 것을 특징으로 하는, 정형 검증 방법
|
| 9 |
9
기록매체에 저장되는 계층적 실시간 스케줄링 시스템의 정형 검증 프로그램으로서, 상기 프로그램은 컴퓨팅 시스템에서 실행되는정형 검증 대상인 상기 계층적 실시간 스케줄링 시스템의 요구 사항을 수신하고, 타임드 오토마타(Timed Automata) 기반의 정형 기법을 이용하여 상기 시스템에서 문제가 되는 부분을 직관적으로 확인할 수 있는 정형 명세를 생성하는 정형 명세 명령어 세트, 및상기 정형 명세를 모델 검사(Model Checking) 도구를 이용하여 검증을 수행하는 정형 검증 명령어 세트를 포함하되,상기 정형 명세 명령어 세트는, 상기 계층적 실시간 스케줄링 시스템의 최상위 스케줄러의 모델을 명세하는 최상위 스케줄러 모델 생성 명령어 세트, 상기 계층적 실시간 스케줄링 시스템의 적어도 하나 이상의 하위 스케줄러 모델을 명세하는 하위 스케줄러 모델 생성 명령어 세트, 및 상기 계층적 실시간 스케줄링 시스템의 적어도 하나 이상의 태스크를 명세하는 태스크 모델 생성 명령어 세트를 포함하고,상기 요구 사항은상기 최상위 스케줄러의 스케줄링 정책과 상기 최상위 스케줄러의 워크로드 정보를 포함하는 최상위 스케줄러 요구 사항,상기 하위 스케줄러의 스케줄링 정책과 상기 하위 스케줄러의 워크로드 정보를 포함하는 제1 하위 스케줄러 요구 사항,상기 하위 스케줄러의 주기, 상기 하위 스케줄러의 주기 중 필요한 실행 시간, 및 상기 하위 스케줄러의 우선순위를 포함하는 제2 하위 스케줄러 요구 사항, 및상기 태스크의 주기, 상기 태스크의 데드라인, 상기 태스크의 시작 오프셋, 상기 태스크의 우선순위, 및 의존성 정보를 포함하는 태스크 요구 사항을 포함하며,상기 하위 스케줄러는 다른 하위 스케줄러 또는 상기 최상위 스케줄러의 하위 계층의 스케줄러이며, 상기 하위 스케줄러가 실행 시간을 모두 소모하지 않고 주기가 종료한 경우에도 상기 하위 스케줄러에 스케줄링을 요청하는 워크로드가 존재하지 않는다면 스케줄링 가능한 것으로 판단하고,상기 의존성 정보는 상기 태스크가 의존하는 의존 태스크를 나타내며,상기 의존 태스크의 실행이 완료되지 않은 경우 상기 태스크에 대한 스케줄링은 요청되지 않는,계층적 실시간 스케줄링 시스템의 정형 검증 프로그램
|
