More Like this

1. Rethinking Tractability for Schedulability Analysis.

   Kunal Agrawal, Sanjoy Baruah (December 2023, Proceedings of the 44th IEEE Real-Time Systems Symposium (RTSS 2023))
2. CANASTA: Controller Area Network Authentication Schedulability Timing Analysis

   https://doi.org/10.1109/TVT.2023.3258746  

   Ikumapayi, Omolade; Olufowobi, Habeeb; Daily, Jeremy; Hu, Tingting; Bertolotti, Ivan Cibrario; Bloom, Gedare (August 2023, IEEE Transactions on Vehicular Technology)
3. 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)

   null (Ed.)
4. 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))
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. 

   more » « less