@inproceedings{8c61c7e90bac4498acc31bcdd071a6f1,
title = "A user-mode scheduling mechanism for ARINC653 partitioning in seL4",
abstract = "seL4 is formally verified for its functional correctness and provides a trusted code base for ARINC 653 partitioning operating systems. ARINC 653 needs a two-level scheduler to enforce temporal isolation between partitions. We cannot modify the scheduler provided by seL4 to adapt ARINC 653, which may invalidate the formal correctness of seL4. Thus, we propose a user-mode scheduling mechanism, where several user threads serve as the partition scheduler and process schedulers. The execution trace result shows that the temporal partitioning can be enforced by this mechanism. We also elaborate the scheduling overheads.",
keywords = "ARINC 653, Hierarchical scheduling, Partitioning, Sel4",
author = "Qiao Kang and Cangzhou Yuan and Xin Wei and Yanhua Gao and Lei Wang",
note = "Publisher Copyright: {\textcopyright} Springer Nature Singapore Pte Ltd. 2017.; International Conference on Computer, Communication and Computational Sciences, ICCCCS 2016 ; Conference date: 12-08-2016 Through 13-08-2016",
year = "2017",
doi = "10.1007/978-981-10-3770-2\_10",
language = "英语",
isbn = "9789811037696",
series = "Advances in Intelligent Systems and Computing",
publisher = "Springer Verlag",
pages = "105--113",
editor = "Singh, \{Vivek Kumar\} and Shailesh Tiwari and Mishra, \{Krishn K.\} and Bhatia, \{Sanjiv K.\}",
booktitle = "Advances in Computer and Computational Sciences - Proceedings of ICCCCS 2016",
address = "德国",
}