상세정보
학술지
Timed Model-Based Formal Analysis of a Scheduler of Qplus-AIR, an ARINC-653 Compliance RTOS
- 발행일
- 201710
- 출처
- IEICE Transactions on Information and Systems, v.E100.D no.10, pp.2644-2647
- ISSN
- 1745-1361
- 출판사
- 일본, 전자정보통신학회 (IEICE)
- 초록
- Qplus-AIR is a real-time operating system for avionics, and its safety and correctness should be analyzed and guaranteed. We performed model checking a version of Qplus-AIR with the Times model checker and identified one abnormal case that might result in safety-critical situations.
- KSP 제안 키워드
- ARINC 653, Formal Analysis, Model checker, Real-Time Operating System, TIMES model, model checking, model-based, safety-critical situations