ESTEREL을 이용한 RTOS Scheduler 의 검증 및 구현 = Verification and implementation of RTOS Scheduler with ESTEREL

국문 초록 (Abstract)

오늘날 RTOS가 운영되는 시스템이 고안정성을 요구 할수록 임베디드 소프트웨어인 RTOS 의 중요성은 날이 갈수록 증대하고 있다. 검증된 RTOS의 개발을 목표로 본 논문에서는 RTOS의 태스크 스케쥴러를 정형명세하고, 정형명세된 스케쥴러가 가져야 하는 몇가지의 검증특성들을 모덜체킹 기법을 통해서 검증하였다. 또한 에스테럴로 정형 명세된 스케쥴러에서 자동 생성된 C 소스를 사용하여 직접 태스크를 스케쥴해 주는 간단한 RTOS 를 제작함으로서 검증된 RTOS 를 제작 할 수 있는 방법을 제시 하고자 한다.

목차 (Table of Contents)

• 요약
• 1. 서론
• 2. 시스템 자연어 명세
• 3. 검증특성의 자연어 명세
• 4. 에스테럴을 이용한 스케쥴러의 정형 명세
• 5. 검증 특성에 대한 정형 명세
• 6. 모델 체킹을 이용한 특성의 검증
• 7. 검증된 스케쥴러의 사용
• 8. 결론 및 향후 연구 과제
• 9. 참조문헌