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 · 2017
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.