For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Timed Model-Based Formal Analysis of a Scheduler of Qplus-AIR, an ARINC-653 Compliance RTOS
Sanghyun YOON Dong-Ah LEE Eunji PAK Taeho KIM Junbeom YOO
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2017/10/01
Online ISSN: 1745-1361
Type of Manuscript: LETTER
Category: Software System
Qplus-AIR, model checking, real-time operating system, safety,
Full Text: PDF(446.6KB)
>>Buy this Article
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.