Model-based verification of a framework for flexible scheduling in the real-time specification for Java

摘要

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.