ages implement a Cheddar program compiler and interpreter. Then scheduling simulation analysis is performed on AADL specifications with hierarchical schedulers.

-   A two-level scheduler for RTSJ

The Real-Time Specification for Java (RTSJ) is a set of interfaces and behavioral specifications that allow for real-time computer programming in the Java programming language. It is modified to allow applications to implement two-level scheduling mechanism where the first level is the RTSJ priority scheduler and the second level is under application control [@Zerzelidis06b; @Zerzelidis10]. They also verify the two-level scheduler for RTSJ using Timed Automata in the UPPAAL tool [@Zerzelidis06]. The *Thread*, *BaseScheduler* (global scheduler), *EDFScheduler*(local scheduler) and other components are presented by timed automata. Five properties are verified on their model. Three of them are to check the correctness of their model: (1) a thread’s priority never takes an invalid value, (2) no thread can block due to locking after it starts, and (3) the system will always select a thread to run with higher absolute preemption level than the system ceiling, unless the selected thread is either currently locking a resource with higher ceiling than its apl or a thread that has just been released. The other two are liveness and deadlock free properties that state the system is livelock free and can never deadlock.

Summary {#sec:summary}
=======

Comparison of Related Work
--------------------------

We summarize the research work on formal specification and verification of separation kernels in [[[Table]{}]{}]{} \[tbl:comparison\_tab\]. In this table, “[[$\divideontimes$]{}]{}” means that the evidence for the data is not available and empty cells mean that the feature is not considered in the work. We compare seven features of them. The column “Target Kernel” is the object specified or verified in each work. The “Objective” shows the concerns of each work, in which *Specification* indicates that the work concen