More Like this

1. Schedulability Analysis of Adaptive Variable-Rate Tasks with Dynamic Switching Speeds

   https://doi.org/10.1109/RTSS.2018.00054  

   Peng, Chao ; Zhao, Yecheng ; Zeng, Haibo ( December 2018 , 39th IEEE Real-Time Systems Symposium (RTSS))
2. Restart-based fault-tolerance: System design and schedulability analysis

   https://doi.org/10.1109/RTCSA.2017.8046320  

   Abdi, Fardin ; Mancuso, Renato ; Tabish, Rohan ; Caccamo, Marco ( August 2017 , IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA))
3. An Optimization Framework for Real-Time Systems with Sustainable Schedulability Analysis

   https://doi.org/10.1109/RTSS49844.2020.00038  

   Zhao, Yecheng ; Zhou, Runzhi ; Zeng, Haibo ( December 2020 , 2020 IEEE Real-Time Systems Symposium (RTSS))
4. Schedulability Analysis of Engine Control Systems With Dynamic Switching Speeds

   https://doi.org/10.1109/TCAD.2019.2951124  

   Liu, Yu ; Peng, Chao ; Zhao, Yecheng ; Li, Yangyang ; Zeng, Haibo ( October 2020 , IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems)
5. Integrating Formal Schedulability Analysis into a Verified OS Kernel

   Guo, Xiaojie ; Lesourd, Maxime ; Liu, Mengqi ; Rieg, Lionel ; Shao, Zhong ( July 2019 , 31st International Conference on Computer Aided Verification (CAV))

   Formal verification of real-time systems is attractive because these systems often perform critical operations. Unlike non real-time systems, latency and response time guarantees are of critical importance in this setting, as much as functional correctness. Nevertheless, formal verification of real-time OSes usually stops the scheduling analysis at the policy level: they only prove that the scheduler (or its abstract model) satisfies some scheduling policy. In this paper, we go further and connect together Prosa, a verified schedulability analyzer, and RT-CertiKOS, a verified single-core sequential real-time OS kernel. Thus, we get a more general and extensible schedulability analysis proof for RT-CertiKOS, as well a concrete implementation validating Prosa models. It also showcases that it is realistic to connect two completely independent formal developments in a proof assistant.