Model-based Verification of a Framework for Flexible Scheduling in the Real-Time Specification for Java
Alexandros Zerzelidis and Andy Wellings
This paper describes a framework for achieving flexible scheduling in the Real-Time Specification for Java (RTSJ), and provides verification of its operation by modelling it as a system of timed automata in the UPPAAL model checker. The proposed approach is a two-level scheduling mechanism where the first level is the RTSJ priority scheduler and the second level is under application control. Minimum, backward-compatible changes to the RTSJ specification are discussed. The only assumptions made are that the RTSJ implementation supports pre-emptive priority-based dispatching of threads, with changes to priorities having immediate effect. The framework model is described and its correctness checked.
BibTex Entry
@inproceedings{Zerzelidis2006a,
address = {New York, NY, USA},
author = {Alexandros Zerzelidis and Andy Wellings},
booktitle = {JTRES '06: Proceedings of the 4th International Workshop on Java Technologies for Real-time and Embedded Systems},
doi = {http://doi.acm.org/10.1145/1167999.1168005},
isbn = {1-59593-544-4},
location = {Paris, France},
pages = {20--29},
publisher = {ACM Press},
title = {Model-based Verification of a Framework for Flexible Scheduling in the Real-Time Specification for Java},
year = {2006}
}