You are here: TUCS > PUBLICATIONS > Publication Search > Formal Development of Real-Tim...
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