BROWSE
Detail
Journal Article
Timed Model-Based Formal Analysis of a Scheduler of Qplus-AIR, an ARINC-653 Compliance RTOS
Cited 2 time in 
Download 14 time
Share 
Download 14 time
Share
- Issue Date
- 2017-10
- Citation
- IEICE Transactions on Information and Systems, v.E100.D, no.10, pp.2644-2647
- ISSN
- 1745-1361
- Publisher
- 일본, 전자정보통신학회 (IEICE)
- Language
- English
- Type
- Journal Article
- Abstract
- 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 Keywords
- ARINC 653, Formal Analysis, Model checker, Real-Time Operating System, TIMES model, model checking, model-based, safety-critical situations