Model-based Verification of a Framework for Flexible Scheduling in the Real-Time Specification for Java

This report describes a framework for achieving flexible scheduling in the Real-Time Specification for Java (RTSJ), and provides verification of its operation by modeling 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 supports a native thread model, and that the underlying real-time operating system supports pre-emptive priority-based dispatching of threads with changes to priorities having immediate effect. The framework model is described and its correctness checked.