ETRI-Knowledge Sharing Plaform

ENGLISH

성과물

논문 검색
구분 SCI
연도 ~ 키워드

상세정보

학술지 Timed Model-Based Formal Analysis of a Scheduler of Qplus-AIR, an ARINC-653 Compliance RTOS
Cited 0 time in scopus Download 12 time Share share facebook twitter linkedin kakaostory
저자
윤상현, 이동아, 박은지, 김태호, 유준범
발행일
201710
출처
IEICE Transactions on Information and Systems, v.E100.D no.10, pp.2644-2647
ISSN
1745-1361
출판사
일본, 전자정보통신학회 (IEICE)
DOI
https://dx.doi.org/10.1587/transinf.2017EDL8090
초록
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.
키워드
Model checking, Qplus-AIR, Real-time operating system, Safety
KSP 제안 키워드
ARINC 653, Formal Analysis, Model checker, Real-Time Operating System, TIMES model, model checking, model-based, safety-critical situations