Modelling and verification of ARINC 653 hierarchical preemptive scheduling
Joint Authors
Fu, Ning
Shan, Lijun
Du, Chenglie
Peng, Han
Liu, Zhiqiang
Source
The International Arab Journal of Information Technology
Issue
Vol. 17, Issue 1 (31 Jan. 2020), pp.99-106, 8 p.
Publisher
Zarqa University Deanship of Scientific Research
Publication Date
2020-01-31
Country of Publication
Jordan
No. of Pages
8
Main Subjects
Information Technology and Computer Science
Abstract EN
Avionics Application Standard Software Interface (ARINC 653) is a software specification for space and time partitioning in safety-critical avionics real-time operating systems.
Correctly designed task schedulers are crucial for ARINC 653 running systems.
This paper proposes a model-checking-based method for analyzing and verifying ARINC 653 scheduling model.
Based on priced timed automata theory, an ARINC 653 scheduling system was modelled as a priced timed automata network.
The schedulability of the system was described as a set of temporal logic expressions, and was analyzed and verified by a model checker.
Our research shows that it is feasible to use model checking to analyze task schedulability in an ARINC 653 hierarchical scheduling system.
The method discussed modelled preemptive scheduling by using the stop/watch features of priced timed automata.
Unlike traditional scheduling analysis techniques, the proposed approach uses an exhaustive method to automate analysis of the schedulability of a system, resulting in a more precise analysis.
American Psychological Association (APA)
Fu, Ning& Shan, Lijun& Du, Chenglie& Liu, Zhiqiang& Peng, Han. 2020. Modelling and verification of ARINC 653 hierarchical preemptive scheduling. The International Arab Journal of Information Technology،Vol. 17, no. 1, pp.99-106.
https://search.emarefa.net/detail/BIM-956141
Modern Language Association (MLA)
Fu, Ning…[et al.]. Modelling and verification of ARINC 653 hierarchical preemptive scheduling. The International Arab Journal of Information Technology Vol. 17, no. 1 (Jan. 2020), pp.99-106.
https://search.emarefa.net/detail/BIM-956141
American Medical Association (AMA)
Fu, Ning& Shan, Lijun& Du, Chenglie& Liu, Zhiqiang& Peng, Han. Modelling and verification of ARINC 653 hierarchical preemptive scheduling. The International Arab Journal of Information Technology. 2020. Vol. 17, no. 1, pp.99-106.
https://search.emarefa.net/detail/BIM-956141
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references : p. 105-106
Record ID
BIM-956141