UPPAAL을 이용한 AUTOSAR OS기반 응용 프로그램의 schedulability 검증

국문 초록 (Abstract)

오늘 날 차량용 전자제어 시스템의 복잡도는 점차 증가하고 있으며 이에 따라 자동차 안전 요구사항과 타이밍에 관한 제약사항들도 증가하고 있다. 현재의 개발 방식에서 타이밍 제약사항에 대한 검증은 주로 구현 단계에서 이루어지고 있다. 개발 완료 단계에서 발견된 설계의 실수는 많은 추가 비용과 시간을 필요로 한다. 이러한 문제를 해결하기 위해 설계 단계에서 시스템의 타이밍 제약사항을 검증하는 연구가 활발히 이루어지고 있다.
본 논문에서는 AUTOSAR OS에서 실행되는 실시간 응용 프로그램에 대한 스케줄 가능성(schedulability)을 분석한다. 이를 위해 AUTOSAR OS의 태스크와 스케줄러, 프로세서의 timed automata 모델을 제시하고, 모델 검사(model checking) 도구인 UPPAAL을 이용하여 스케줄 가능성을 자동화 검증 및 시뮬레이션 한다. AUTOSAR OS는 OSEK/VDX OS를 기반으로 동작하며 timed automata 모델링을 위해 OSEK/VDX OS 표준을 따른다. 제시하는 timed automata 모델은 단일 프로세서, 고정 우선순위 선점형 스케줄러, 고정 릴리즈 오프셋을 가진 주기적 태스크, 혼합 선점형 스케줄링 정책과 자원 공유를 위한 우선순위 상한 프로토콜을 고려하였다. 모델의 간략화와 직관성을 높이기 위해 UPPAAL 4.1에서 지원하는 스톱워치(stop-watch) 기능을 적용하였으며, 검증 결과로 스케줄 가능성 여부와 태스크 당 최악의 응답시간(worst case response time), 반례(counter example)을 얻을 수 있다. 모델 검사에서 발생하는 상태 공간 폭발 문제를 완화하는 수준의 추상화된 모델을 제시한다. 마지막으로 본 논문에서 제시한 모델에 예제 시스템을 적용하여 스케줄 가능성을 분석하고 설명한다.

목차 (Table of Contents)

• 1. 서론 1
• 2. 관련 연구 4
• 3. UPPAAL 7
• 4. OSEK/VDX OS 11
• 4.1. Task Management 11
• 4.2. Conformance Class 12
• 4.3. Scheduling Policy 13
• 4.4. Resource management 13
• 5. AUTOSAR OS 모델링 및 검증 15
• 5.1. AUTOSAR OS 모델의 구성요소 15
• 5.2. UPPAAL 모델 설명 16
• 5.2.1. Task Template. 18
• 5.2.2. Processor Template 25
• 5.2.3. Scheduler Template 28
• 5.3. 검증 속성 30
• 5.4. 검증 결과 31
• 6. 결론 및 향후 연구 36
• 7. 참고문헌 38