Skip to main navigation Skip to search Skip to main content

Towards Fault-Tolerant Real-Time Scheduling in the seL4 Microkernel

  • Beihang University
  • Science and Technology on Communication Networks Laboratory

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

System dependability and real-time requirement have been receiving widespread attention in modern computer systems. Fault-tolerant real-time scheduling provides a method of combining timing requirements and faults tolerance for real-time systems. This paper presents a preliminary study of building a fault-tolerant real-time mechanism for seL4 microkernel. seL4, as the first formally-verified operating system kernel in the world, is an ideal platform for security-critical systems. However, the lack of real-time and fault-tolerant policy reduces its the reliability and user experience. We have implemented basic real-time and checkpoint mechanisms in seL4, and propose the Check-Point based Fault-Tolerant RM (CP-FTRM) scheduling policy. The experiments have shown the feasibility and efficiency of them.

Original languageEnglish
Title of host publicationProceedings - 18th IEEE International Conference on High Performance Computing and Communications, 14th IEEE International Conference on Smart City and 2nd IEEE International Conference on Data Science and Systems, HPCC/SmartCity/DSS 2016
EditorsLaurence T. Yang, Jinjun Chen
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages711-718
Number of pages8
ISBN (Electronic)9781509042968
DOIs
StatePublished - 20 Jan 2017
Event18th IEEE International Conference on High Performance Computing and Communications, 14th IEEE International Conference on Smart City and 2nd IEEE International Conference on Data Science and Systems, HPCC/SmartCity/DSS 2016 - Sydney, Australia
Duration: 12 Dec 201614 Dec 2016

Publication series

NameProceedings - 18th IEEE International Conference on High Performance Computing and Communications, 14th IEEE International Conference on Smart City and 2nd IEEE International Conference on Data Science and Systems, HPCC/SmartCity/DSS 2016

Conference

Conference18th IEEE International Conference on High Performance Computing and Communications, 14th IEEE International Conference on Smart City and 2nd IEEE International Conference on Data Science and Systems, HPCC/SmartCity/DSS 2016
Country/TerritoryAustralia
CitySydney
Period12/12/1614/12/16

Keywords

  • Checkpoint
  • Fault-tolerance
  • Rate monotonic algorithm
  • Real-time system
  • SeL4
  • Time redundancy

Fingerprint

Dive into the research topics of 'Towards Fault-Tolerant Real-Time Scheduling in the seL4 Microkernel'. Together they form a unique fingerprint.

Cite this