Where academic tradition
meets the exciting future

Formal Development of Real-Time Priority-Based Schedulers

Cristina Cerschi Seceleanu, Formal Development of Real-Time Priority-Based Schedulers. In: Tim O'Neill Jerzy Rozenblit, Jianfeng Peng (Eds.), Proceedings of the 12th IEEE International Conference on the Engineering of Computer-Based Systems (ECBS 2005), Greenbelt, Maryland, USA, 263-270, IEEE Computer Society Press, 2005.

Abstract:

We propose a method for constructing real-time scheduling programs, based on continuous action systems and the higher-order logic of the refinement calculus. The schedulability goal is a guarantee that all the tasks meet their deadlines, at run-time. This analysis reduces to checking that "always" temporal properties hold on the task set, by enforcing adequate invariance properties. The initial, conjunctive model of the real-time system is further transformed, through refinement, into a program that obeys a specific scheduling policy. We exemplify our method on the Deadline-Monotonic and the Earliest-Deadline-First algorithms.

BibTeX entry:

@INPROCEEDINGS{inpCerschiSeceleanu05a,
  title = {Formal Development of Real-Time Priority-Based Schedulers},
  booktitle = {Proceedings of the 12th IEEE International Conference on the Engineering of Computer-Based Systems (ECBS 2005), Greenbelt, Maryland, USA},
  author = {Cerschi Seceleanu, Cristina},
  editor = {Jerzy Rozenblit, Tim O'Neill and Jianfeng Peng},
  publisher = {IEEE Computer Society Press},
  pages = {263-270},
  year = {2005},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication