 of two-level scheduling and correct implementation of the scheduler. The first one usually uses a compositional approach to formally specify and analyze the schedulability of real-time applications running under the two-level scheduling. The recent work is discussed in [@Carnevali11; @Carnevali13]. It considers the application but not the separation kernels. Our survey concerns with verification of separation kernels and the second one is discussed here.

-   Honeywell DEOS scheduler

The Honeywell Dynamic Enforcement Operating System (DEOS) is a microkernel-based real-time operating system that supports flexible IMA applications by providing both space partitioning at the process level and time partitioning at the thread level. The model checking and theorem proving approaches have been applied to the DEOS scheduler to analyze the temporal separation property [@Penix00; @Penix05; @Ha04].

A core slice of the DEOS scheduling kernel contains 10 classes and over 1000 lines of actual code are first translated without abstraction from C++ into Promela, which is the input language for the Spin model checker. The temporal partitioning property of DEOS scheduler is that each thread in the kernel is guaranteed to have access to its complete CPU budget during each scheduling period. They use two approaches to analyze the time partitioning properties in the DEOS kernel. The first one is to place assertions over program variables to identify potential errors. The second approach is to use a liveness property, *Idle Execution*, presented by LTL. The liveness property specified as $ \mathrm{[\;](beginperiod -> (! \; endperiod \; U \; idle))}$, states that if there is slack in the system (i.e., the main thread does not have 100% CPU utilization), the idle thread should run during every longest period. This is a necessary condition of time partitioning.

The size and complexity of this system limit them to analyze only one configuration at a time. To overcome this limitation and generalize the analysis to arbitrary configurati