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   Vol.E100-D   No.10   pp.2644-2647
Publication Date: 2017/10/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2017EDL8090
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.