Formal analysis of aperiodic and sporadic real-time threads in the RTSJ

The Real-Time Specification for Java (RTSJ) provides an integrated approach to scheduling real-time threads and asynchronous event handlers. The behaviour of these schedulable objects can be defined by the association of different types of parameter objects with each instance. For example, the ReleaseParameter class hierarchy allows a schedulable object to indicate whether it should be released periodically or aperiodically. Although the RTSJ provides a general scheduling framework for schedulable objects, only asynchronous event handlers can have the full range of release parameters. The model for real-time threads is well-defined for periodic releases but lacks the support needed for aperiodic releases. Recently, the Expert Group have proposed the addition of several methods in the RealTimeThread class to allow better integration with the ReleaseParameter class hierarchy. This paper uses model checking techniques to evaluate the coherence and consistency of the proposed approach.