Requirement specification and model-checking

of a real-time scheduler implementation

Khaoula BOUKIR Jean-Luc BÉCHENNEC Anne-Marie DÉPLANCHE
khaoula.boukir@ls2n.fr jean-luc.bechennec@ls2n.fr anne-marie.deplanche@ls2n.fr
University of Nantes CNRS University of Nantes
Nantes, France Nantes, France Nantes, France
ABSTRACT to first study the feasibility of their implementation within a real
Implementing a new scheduler within a real-time operating system platform and to evaluate their true performances. In this context,
is challenging. The transition from a theoretical scheduling policy our goal is to extend our RTOS Trampoline [5] so that it can support
specification to a real platform implementation requires several global multiprocessor scheduling policies.
constraints to be taken into account. Therefore, a verification pro- In the current design of Trampoline, the integration of new
cess must support the implementation work to give it a level of schedulers is kernel-based. However, scheduler implementation at
confidence and validate its correctness. the kernel level is not an easy task: it requires a complete under-
In this paper, we present such a verification approach which standing of the OS architecture and code. Multiple implementation
is based on model-checking. It aims to identify subtle issues in constraints which are completely abstracted in literature must be
our implementation of scheduling policies within an OSEK/VDX considered and the gap between theoretical scheduling specification
real-time operating system called Trampoline. As an example, the and concrete RTOS considerations makes the scheduler program-
approach is conducted on elaborated models of an implemented ming task complex.
G-EDF scheduler along with other OS components that contribute This gives rise to many issues: how to ensure that the imple-
to the scheduling decision. Then, the verification is carried out mentation of a new scheduling policy within an RTOS is correct?
by checking a set of relevant requirements which are identified How to verify that the implemented scheduler always produces the
based on the expected behavior of the scheduler as specified in the expected behavior in accordance with the specifications given in
literature. This approach demonstrated its feasibility since potential theory? What are the effective means to verify this correctness and
issues are detected in our implementation. how to establish an efficient approach for this verification? In fact,
if we want theoretical results in real-time scheduling to emerge in
CCS CONCEPTS practice, implementations should be supported with verification
methods that can provide confidence on their functional correctness.
• Computer systems organization → Real-time operating sys-
Manual verification cannot be an option considering the implemen-
tems; • Theory of computation → Verification by model checking.
tation complexity and constraints. A possible approach to detect
KEYWORDS implementation errors is simulation under significant scenarios.
However, one cannot identify all possible scenarios that the system
Model-checking, RTOS, Implementation, scheduler must deal with.
ACM Reference Format: In order to address this problem, we aim to use formal approaches
Khaoula BOUKIR, Jean-Luc BÉCHENNEC, and Anne-Marie DÉPLANCHE. to formally verify the implementation of global scheduler within a
2020. Requirement specification and model-checking of a real-time scheduler real-time operating system. To do so, we focus on verifying require-
implementation. In 28th International Conference on Real-Time Networks and
ments of the implemented scheduler. Our study is not intended to
Systems (RTNS 2020), June 9–10, 2020, Paris, France. ACM, New York, NY,
verify the schedulability of an application but rather to verify the
USA, 11 pages. https://doi.org/10.1145/3394810.3394817
behavior of the scheduler implementation. Our approach is based
1 INTRODUCTION on a previously elaborated model of an implementation of G-EDF
in Trampoline [10]. This model describes carefully the control flow
Adopting multicore architectures for executing real-time appli-
of the implementation since it abstracts every instruction of the
cations has given rise to multiple research projects in order to
source code into a transition in the model using the same variables
propose efficient scheduling policies [3]. This has motivated some
and actions of the implementation.
new works of implementing dynamic scheduling policies such as
EDF [11, 15, 22]. However, to adopt such policies, it is essential Contribution and outline: The work described in this article
presents a formal approach that addresses the issue of verifying
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
the correctness of a global scheduler implementation within the
for profit or commercial advantage and that copies bear this notice and the full citation purpose-built embedded Trampoline RTOS. The main idea is to
on the first page. Copyrights for components of this work owned by others than ACM provide evidence that the implemented scheduler behavior matches
must be honored. Abstracting with credit is permitted. To copy otherwise, or republish,
to post on servers or to redistribute to lists, requires prior specific permission and/or a its specifications.
fee. Request permissions from permissions@acm.org. This study is the follow-up of a prior work where an implemen-
RTNS 2020, June 9–10, 2020, Paris, France tation of G-EDF scheduler within Trampoline, that only supported
© 2020 Association for Computing Machinery.
ACM ISBN 978-1-4503-7593-1/20/06. . . $15.00
static partitioned scheduling, was proposed. This previous work
https://doi.org/10.1145/3394810.3394817 was also associated with initial ideas to verify the implementation.
RTNS 2020, June 9–10, 2020, Paris, France K.Boukir, et al.

[10]. However, the verification was partial and performed for one time Petri nets, and on state space analysis methods. Another study
application which does not guarantee an exhaustive verification of [24] of modeling an OSEK/VDX application and the core part on its
the scheduler. Our rational in this paper is to rather use the previ- kernel have been proposed, it uses UPPAAL[7] to perform rigorous
ously achieved implementation and conduct a modular verification timing analysis. Bodeveix et al. [8] used also model-checking to
approach on it based on specific requirements. These requirements verify some scheduler properties within BOSSA framework [4] as
are identified in accordance with the expected behavior of the im- well as several safety properties of the OS. This formal method
plementation and demonstrated to be significant for it. They are has been also applied in hardware and software verification. For
verified using model-checking to ensure that the implementation instance, Intel has been using it since 1990 to build industrial verified
is compliant with the scheduler’s specifications. To do so, verifica- systems [2, 17]. It has also reported the success of this technique to
tion engines are elaborated to generate all possible scenarios for detect programming errors that would have been escaped all the
activating and executing a given task set. verification tools.
The rest of this paper is organized as follows. Section 2 discusses Our rationale for employing formal verification is quite different
related works. Section 3 provides a review of the initial work of from the works presented above: given a scheduler implemented
this study. Section 4 explains the choice of requirements to be inside an RTOS kernel, we aim at checking the correctness of its
verified for the implementation. Section 5 presents our approach implementation formally based on a model. By correctness, we
for conducting verification of these requirements and Section 6 mean not only the absence of programming errors that are likely to
illustrates some of its results. crash the OS, but also the accuracy of the scheduling operations and
decisions. It is a similar objective that can be found in [20]. In the
2 RELATED WORKS context of a meta scheduler for implementing real-time scheduling
There have been a number of works using formal methods to verify algorithms on POSIX compliant RTOS, model-checking is used to
real-time operating systems regarding various problems. Funda- ensure that the outputs from a scheduling algorithm using the meta
mentally two main approaches are being used: scheduler framework conform to the scheduling decisions of its
native version implemented inside the kernel. This study however,
Theorem proving: is a formal method characterized by describing does not consider the multicore/multiprocessor constraints, and
the specification of a system in a mathematical reasoning system, the verification is conducted on one application. Our verification
which consists of a set of axioms and a set of inference rules that can work on the other hand, aims to verify the implementation of a
be used to derive new theorems. In the field of OS kernel verification, global multiprocessor scheduling policy regardless of any specific
this approach has been used to verify SeL4 [19] and CertikOS [18]. task. It is rather in line with the work of Tigori et al [23] where the
Both are certified OSs using interactive theorem proving although whole platform independent source code of Trampoline is modeled
they don’t support real-time applications. SeL4 is a micro-kernel as a network of extended finite automata. By adding an application
that uses the theorem prover Isabelle/HOL [21]. CertikOS uses the model and doing a reachability analysis, the operating system can
Coq proof assistant [14] for its certification. be configured so that all the dead code is removed. In [6] the model
The theorem proving was also used in numerous works that are is extended with observers to verify the OSEK/VDX conformance
interested in studying the schedulability within a real-time operat- of the configured operating system.
ing system. The work around Prosa for instance [13] addresses the
response time analysis for global fixed priority and EDF schedulers 3 BACKGROUND
and provides a flexible foundation for formally proven schedula-
This section provides a summary of the work previously carried
bility analysis based on mechanized proofs. This work does not
out [9, 10] to implement and model a G-EDF scheduler within
match with our objective since we are interested in the verification
Trampoline RTOS [5].
of implementations and not in the analytical aspects of real-time
systems.
3.1 Implementation of G-EDF
The aforementioned verification approaches require user guid-
ance and the specification of many lemmas and a large number of Trampoline1 [5] is an open source real-time operating system that
commands. This demands a significant expertise in the field and a implements the OSEK/VDX and AUTOSAR standards. It was devel-
large human investment to prove small theorems, which gets worse oped in the Real-Time Systems group at LS2N in Nantes (France).
in the event of proving sophisticated properties. Initially, it supported partitioned scheduling in multicore. Trampo-
line’s scheduler is implemented at the kernel level. This means that
Model-checking: is an automated formal verification approach multiple components and functions of low-level are involved in
that allows the exploration of all possible states that the verified calculating the scheduling decision and they define the scheduling
system can go through and checking desirable properties over its perimeter. These components are detailed below (cf. Fig. 1).
state-space. Thanks to its advantages, model-checking has been Task Manager: it gathers low-level functions that are responsi-
successfully applied in numerous research works related to the ble for activating and terminating jobs.
field of real-time systems. Those related to scheduling have as Time Manager: it handles the calculation, the representation
their objective either to verify the schedulability of a system [16], and the comparison of absolute deadlines.
or to build a scheduler tailored to a particular system using the Task List Manager: it handles all the operations related to the
paradigm of controller synthesis [1]. For the most part, they are insertion and extraction of ready jobs into task lists on the request
based on the theory of timed models such as timed automata or
1 http://trampoline.rts-software.org
Requirement specification and model-checking of a RT scheduler implementation RTNS 2020, June 9–10, 2020, Paris, France

of Task Manager or the Scheduler. It also takes in charge of sorting by core. Each one contains the running, elected and need_switch
these lists. fields: - running gives the identifier of the running task, - elected
Scheduler: it is responsible for determining the scheduling se- contains the identifier of the task that is selected by the Scheduler
quence according to G-EDF policy. It is called by Task Manager and, - need_switch indicates if a context switching must take place.
whenever a job is activated or terminated. Note that in the multi-core version of Trampoline, there is only
Context Switch Manager: performs the context saving of the one instance of the OS that runs sequentially in the cores in which
job that is preempted and restores the context of the one that gains the OS should be executed. Thus, the access to the kernel by a core
the CPU following the Scheduler’s decisions. is sequentialized due to a global lock that prevents competition
between cores. It is important to note that the main purpose of
this paper is not to propose an implementation of G-EDF scheduler.
Thus, for more details about this implementation please refer to
[9, 10].
3.1.2 Scheduling procedure. In our implementation of G-EDF,
only basic and independent tasks are considered. Meaning that
we do not focus on tasks that can wait for events or share re-
sources. Thus, the scheduler is triggered only for job activation or
completion. The steps for making the scheduling decision within
Trampoline are summarized below:

Figure 1: Interactions of G-EDF scheduler with other Tram- 1. When a scheduling event occurs and it is a new job activation
poline’s components. of a task 𝜏𝑖 , the absolute deadline of the job is computed by the Time
The scheduling decision is calculated by the Scheduler using Manager. If the activation count indicates that there is already an
the informations provided by the Task List Manager and the active job for that task, the Task Manager calls the Task List Man-
Time Manager ager in order to store the new activated job in the PendingJobList𝑖
along with its absolute deadline. Otherwise, the job is stored in the
ReadyList according to its absolute deadline and the Task Manager
3.1.1 Some Trampoline features. In Trampoline’s G-EDF sched- puts the task 𝜏𝑖 in the READY state. If the scheduling event is a termi-
uler, an absolute deadline is computed whenever a job is activated nation, the PendingJobList𝑖 of the terminated task 𝜏𝑖 is checked. If
by adding its corresponding relative deadline to the current time. there is a pending job, it is removed from the PendingJobList𝑖 and
The time in Trampoline is represented on a circular time model stored in the ReadyList according to its absolute deadline. In that
with 32-bit variable and 1𝜇s resolution. The comparison of dead- case the state of the task is changed to READY, otherwise it becomes
lines is performed using the ICTOH algorithm (for Circular Timer’s SUSPENDED. In the end, the Task Manager calls the Scheduler.
Overflow Handler) [12].
Trampoline OS allows successive activations of the same task 2. When the Scheduler is called, it selects the highest priority
up to a statically fixed limit that is called the maximum activation jobs by consulting the ReadyList and the absolute deadlines of
count. This means that the release of a new job of a task may occur jobs calculated by the Time Manager. In the implementation, the
ReadyList is sorted in an increasing absolute deadlines order. There-
even if the previous one did not terminate. The number of jobs
activated for a task and not yet completed is called the activate fore, the Scheduler must only select the 𝑚 jobs from the head of the
ReadyList to be executed on the 𝑚 free processors. To do so, two
count. However, two jobs of the same task should not be executed
at the same time and the priority of execution shall be attributed tests are iteratively performed: 1) is there a free processor while the
ReadyList is not empty? 2) does the job at the head of the ReadyList
to the oldest released job. For this purpose, two types of ready job
lists are considered: 1) the ReadyList: to store the oldest released has a higher priority than the running one? In the first case, the
and non-terminated ready jobs of each task that we call active jobs. job at the head of the list is extracted to be executed on the free
It is implemented as a min heap in which absolute deadlines of jobs processor. In the second case, the running job is preempted, put
are used as keys (values of the nodes). If several jobs have the same back in the ReadyList and its state is changed to READY. Then, the
deadline, they are attached as a linked list to the same heap node. higher priority task is extracted and scheduled for execution.
2) the second type is used to store new released jobs of a task while 3. When the scheduler decides that a context switch shall take
the previous one is not terminated. They are called pending jobs. place on a core, it updates elected and sets need_switch in the
Each task 𝜏𝑖 has its own list PendingJobList𝑖 . It is implemented as a corresponding tpl_kern. Then, the Context Switch Manager saves
FIFO according to the task activation order and it stores its pending the context of the task identified in running, loads the context of
job absolute deadlines. the one given by elected, copies the value of elected into running
In Trampoline, the scheduling operations always take place on and the state of the task becomes RUNNING.
the core where the scheduling triggering event occurs. However,
rescheduling may lead to a preemption and a context switching
that have to be achieved on another core. So as to separate jobs
that are considered by the scheduler from the actual ones that are
running on processors, the tpl_kern structures are available, one
RTNS 2020, June 9–10, 2020, Paris, France K.Boukir, et al.

3.2 Implementation modeling

3.2.1 General modeling techniques. Our work concerns only
the implementation of the scheduler and does not focus on model-
ing the entire OS. As a result, a pre-existing OS model proposed by
Tigori and al. [23] is used as a basis for building models concerning
our implementation. The OS model is elaborated using UPPAAL
model-checker [7] which accounts for the use of it in our work.
In the models, each Trampoline’s function is abstracted by an Ex-
tended Finite Automaton (EFA) or by a function written in UPPAAL
language (a syntax similar to C language) using the following rules:
• the structure of the automaton describes the control flow of
the modeled system.
• the variables used in the model are the control variables of
the system.
• a sequence of instructions is abstracted by a single action
with a set of updates and/or guards on the set of variables.
In such a case, their execution is considered “atomic”.
• actions and conditions on variables attached to each transi- Figure 2: part of the Scheduler automaton: Double circle rep-
tion are the same ones that correspond to the source code of resents initial location, the ∪ inside a location denotes an
the system. urgent location and each location describes the function ex-
• the imperative code associated with each transition of the ecution state. Guards are depicted in green, synchronization
automaton is similar to the source code of the system. in light blue and actions in dark blue.
In every automaton of the OS model, a transition corresponds
either to a test or an action (an assignment or a function call). The on the free cores available. The second one is used to check if there
transition can be firable only if the test is satisfied, and as soon as is a job stored in the ReadyList which has a higher priority than a
it is fired, the associated action is performed. running job. A part of the scheduling function model is illustrated
Tests are translated to a guard and assignments by an update in Fig 2. This part first describes the process of comparing the
over the control variables. Function calls are handled by a synchro- deadlines of the running task (the one in the head of the ReadyList
nization mechanism between the two automata. First, the caller (front_task)) and the preemption of the running task if it has lower
automaton releases the execution of the callee automaton with a priority followed by the execution of the front_task.
synchronization over a channel (with “!” to emit and “?” to receive)
and sets a shared variable to 0. A guard using this variable blocks 3.2.3 Timer model: The G-EDF scheduler is based on deadlines
the caller while it is equal to 0. Second, the callee automaton com- to perform the scheduling. Thus, it is necessary to model a mecha-
pletes its instructions and sets the shared variable to 1 to release nism that allows retrieving the current time in order to calculate
the caller. This ensures the sequential execution conforming to the the absolute deadlines. To do so, a timed automaton that models a
real execution. The function parameters are passed from the caller Timer is considered. It uses a clock variable to represent the pro-
automaton to the callee automaton by using shared variables. gression of time. The automaton handles also a shared variable that
In the model, the kernel is considered untimed. Each state, except represents the time in microseconds (as in the real implementation
the initial state, of an automaton is urgent. Accordingly, from the in Trampoline). This variable is incremented whenever the Timer
point of view of the other components of the system, the execution automaton is synchronized with other automata in which passing
of a sequence of kernel code is performed in zero time. In fact, taking time is needed as shown in 3. It is necessary to distinguish this
into account the OS execution overheads can be useful in the case of Timer which is used only in the model for time progression, from
checking whether or not the deadlines are met as in schedulability the Time Manager which is an OS component responsible for the
analysis. This does not interfere with our objectives since we aim calculation and comparison of absolute deadlines.
to verify the functional aspect of the G-EDF implementation. Thus,
our model does not consider overheads and only elapses time while 4 REQUIREMENTS SPECIFICATION
tasks are being executed but not at the kernel level. G-EDF is a work-conserving and fixed job priority policy. The prior-
ity assignment is based on the absolute deadlines of jobs. Therefore,
3.2.2 G-EDF model. Using the rules described above, the imple-
the implemented scheduler must ensure that at any time 𝑡, it is
mented functions of the components involved in the scheduling
the 𝑚 jobs (at most) with the closest absolute deadlines that are
are modeled using EFAs. Due to space limits, we only present EFAs
running on the 𝑚 processors. It is expressed by the two following
abstracting the Scheduler and the Timer functioning.
requirements:
In the model, the scheduling function tpl_schedule() is executed
whenever the EFA that models the Task Manager is synchronized • at any time 𝑡, all the tasks that are in the RUNNING state have
with the Scheduler’s EFA. Then, the scheduling is performed in two smaller absolute deadlines compared to any other task in the
loops. The first one is used to start the highest priority ready jobs READY state.
Requirement specification and model-checking of a RT scheduler implementation RTNS 2020, June 9–10, 2020, Paris, France

each component and to better locate implementation errors. For

every component, a set of requirements is specified according to
its expected behavior. We distinguish intrinsic requirements that
depend on the G-EDF policy and could be reused for another im-
plementation of the policy in another operating system. On the
other hand, we also consider requirements that depend on how
Trampoline is designed and that must be re-adapted according to
the implementation platform.
Task Manager: ensures that the necessary functions for activa-
tions or terminations of jobs are performed correctly. The require-
ments that must be verified are:
Figure 3: the Timer automaton: The timer emits a call through - when a job of a task i is activated:
a synchronization on a broadcast channel MicroSecondesInc!. • if the activation count of task i is zero, the new activated job
𝐼𝑆_𝐾𝐸𝑅𝑁 𝐸𝐿_𝑀𝑂𝐷𝐸 () is a function used as a transition guard to shall be put in the ReadyList.
make sure that the execution is not at the kernel level since • if the activation count of task i is zero, the task’s state shall
the kernel is untimed. When it is fired, it calls a function become READY_AND_NEW.
micro_secondes_inc_func() to increment the time variable in 𝜇s. • if the activation count of task i is greater than 0 and less than
its maximum activation count, the new activated job shall be
put in the PendingJobList𝑖 .
• a processor cannot be free while there is at least one task in • if the activation count of task i is equal to its maximum acti-
the READY state. vation count, the new activated job shall be ignored.
• if the activation count of task i is less than its maximum acti-
4.1 Taking implementation specification into vation count, it shall be incremented.
account - when a job of a task i is terminated:
When moving to the actual implementation of G-EDF policy in • the activation count of task i shall be decremented.
Trampoline, other requirements have to be taken into account. As • if the activation count of task i is equal to 1, the task’s state
presented in 3.1, the scheduling decision within Trampoline in- shall become SUSPENDED.
volves other components of the OS other than the Scheduler. There- • if the activation count of task i is greater than 1, the task’s
fore, checking the correct functioning of these components cannot state shall become READY.
be ignored. Even if the Scheduler operates correctly according to • if the activation count of task i is greater than 1, the oldest
the requirements expressed above, the produced scheduling result pending job shall be removed from the PendingJobList𝑖 and
might be false if the behavior of the other components is wrong. put in the ReadyList.
In our implementation, we can highlight some situations that may - for every job activation or termination of task i:
occur:
• if the activation count of task i is greater than 0, the size of the
situation 1: the Task Manager does not call the Scheduler after PendingJobList𝑖 shall be greater than 0.
a job activation or termination. Thus, the scheduling is not • if the ReadyList does not contain a job of task i and no job of
performed. task i is running, the PendingJobList𝑖 shall be empty.
situation 2: the Task Manager does not put a new activated job of • the Scheduler shall be called.
task 𝜏𝑖 in the ReadyList or the PendingJobList𝑖 . In that case,
the Scheduler’s decision does not take into account this new Time Manager: these functions handle the computation and the
activated job. comparison of absolute deadlines which are used to store ready jobs
situation 3: the Task Manager miscalculates the activation count in the ReadyList and PendingJobLists. To ensure that the ReadyList
of a task. Then, the jobs can be lost during the process of is sorted according to the correct deadline, the following require-
scheduling. ments must be checked:
situation 4: the Context Switch Manager does not apply the sched- • absolute deadlines are computed according to the ICTOH algo-
uling decision computed by the Scheduler. In that case, the rithm.
following rescheduling will be based on false results. • absolute deadlines are compared correctly according to the
In order to take into account such situations, behavioral require- ICTOH algorithm.
ments to analyze the proper functioning of the system components Task List Manager: As the scheduler is implemented to select the
must be expressed. m jobs at the top of the ready list to execute them, it is necessary to
ensure that these jobs are precisely the highest priority ones ie. the
4.2 OS components requirements ReadyList and the PendingJobLists must be managed as expected.
Our approach consists of carrying out the verification in a modular To this end, the following requirements are considered:
way by verifying separately every component of the scheduling
perimeter. It leads to clearly delimit the verification perimeter of
RTNS 2020, June 9–10, 2020, Paris, France K.Boukir, et al.

• when the Scheduler is called, the ReadyList and all of the

PendingJobLists shall be sorted in an increasing absolute dead-
line order.
• 2 nodes of the heap implementing the ReadyList shall have
distinct keys.
Scheduler: these requirements are used to check whether the final
results of the scheduling are consistent with what is expected or
not:
• during the execution the m jobs in the RUNNING state have
always a lower absolute deadline than any other job in the
ReadyList or any of the PendingJobLists.
Figure 5: Structure of an observer
• a processor shall never be idle while the ReadyList or the
PendingJobList are not empty.

Context Switch Manager: to check that the context switching 5.1 Observer models
is always performed based on the Scheduler’s command. Then, we The previously presented requirements are complex and some of
can simply verify that: them depend on the implementation choices. The expression of a
• the context switching shall be performed according to the Sched- CTL formula verifying one of them quickly becomes complicated
uler decisions. and requires the nesting of several sub-formulas into a single one
with an exponential size. Especially when dealing with a ReadyList
5 VERIFICATION APPROACH of 𝑛 tasks and 𝑛 PendingJobLists at most. Therefor, we choose to
check them using observer models and express properties on their
Our approach consists of checking the implementation correctness
states.
during the execution of the OS model over a time interval driven
The observer models are EFAs with committed states. These
by the Timer Model. The complete model (OS + Timer) is stimulated
states are priority states, which means that if there are several
using task activation and termination scenarios generated by what
fireable transitions, the transition related to the committed states is
we call verification engines (cf. 5.3). The verification of the complete
fired before the others. This makes it possible to check the system
model is carried out by checking the requirements introduced in
without the risk of altering its evolution.
section 4.2. They are checked using observers that run in parallel
Each observer describes a set of requirements used to check an
with the complete model to observe its behavior. Since our goal is
OS component. All the observers inserted in our model have the
to carry out the verification in a modular way, an observer per OS
same structure shown in Fig. 5. The execution of an observer is
component is elaborated (cf. 5.1). Then, reachability properties are
launched when receiving a synchronization Trigger_synch? from
expressed in CTL (Computation Temporal Logic) and checked on
the system notifying that the corresponding component ended its
the observer states to verify that the system is behaving as required.
execution. The Verification Box is the part of the observer that helps
The properties are all expressed in a identical way, they are stated
checking the desired requirements using a set of test functions.
in Section 5.2. A combination of observer models and the complete
Each requirement is translated to a test function that returns true
system model is formed and inserted as input to the UPPAAL model-
or false depending on the result of meeting the requirement. When
checker (VerifyTA) along with expressed properties. The model-
a requirement does not hold, the corresponding output transition
checker verifies if the given properties describing the expected
leads to a Bad state of the system. On the other hand, if all the
behavior hold, or else it generates a counterexample scenario with
requirements are satisfied, output transition leads to a Good state
the corresponding execution trace (cf. Fig. 4).
and the observer goes back to its initial state to wait for the next
trigger.
Figure 6 shows the observer used to verify the Scheduler. It is
called to check if the two intrinsic requirements of G-EDF scheduler
hold: the priority and the idleness check.
For the verification of the first requirement concerning the prior-
ity, the observer uses the synchronization end_run_elected[core_id]?
to wait for the function tpl_run_elected() to be executed. This syn-
chronization is to ensure that the observer does not permanently
check the associated requirements since there are system states that
are not significant for it. Note that the tpl_run_elected() function
changes the state of the task elected by the scheduler to RUNNING
state and load its context for execution. Thus, at the end of the
execution of this function, the observer checks whether the task
Figure 4: Formal verification process that is being set for execution has a shorter deadline than any
other task in the ReadyList or in a PendingJobList. This function is
Requirement specification and model-checking of a RT scheduler implementation RTNS 2020, June 9–10, 2020, Paris, France

Requirements of the scheduler component Test function Formal property

"during the execution the m jobs in the RUNNING state have always a lower absolute deadline check_edf_prio()
E <> Scheduler_Observer.Bad
than any other job in the ReadyList or any of the PendingJobLists"
a processor shall never be idle while the ReadyList or the PendingJobList are not empty. check_idle_cores()
Table 1: Scheduler requirements formal specification

The property is expressed in CTL language using two types of

logic operators:
• quantifiers over all paths: like 𝐴(𝜙) to express that 𝜙 holds
along all execution paths (inevitably); 𝐸 (𝜙) for 𝜙 holds along
at least one path (possibly).
• quantifiers over a specific path: like 𝐺 (𝜙) to say that 𝜙 holds
on the entire subsequent path (globally); 𝐹 (𝜙) to say that 𝜙
eventually holds somewhere on the subsequent path (finally).
In UPPAAL, these quantifiers are expressed using the syntax
[] and <> respectively.
For every observer, the logic operators are used to express two
types of reachability tests: 1) we check if all paths lead finally to the
Good state (A <> Observer.Good), 2) we verify if there exists a path
leading to a Bad observer state (E <> Observer.Bad). If a property is
not verified, the error can be detected by following the transition
Figure 6: The Scheduler’s observer that led to the Bad state and a simulation trace generated by UPPAAL
model-checker. Table 1 illustrates the formal specification of the
scheduler requirements.
always executed on the core where the elected task must be run-
ning. Therefore, the observer is parameterized by the identifier of 5.3 Verification engines
the core on which the function is executed. This is specific for a In pursuance of verifying the requirements over the elaborated
multi-core system verification. It prevents being in the situation models, the Scheduler must be triggered and forced to operate in
of checking the requirement for a core that has not yet finished different situations and scheduling events. For this purpose, an
loading the context of its elected task. Once the observer is syn- element which is responsible for generating different scenarios to
chronized with the tpl_run_elected() function, the priority check call and operate our Scheduler is built. This element is called the
of the elected task is performed at the Prio_Check state. If the test verification engine. The idea is to generate for a given number 𝑛 of
is satisfied, the observer goes to the Inter state. It is possible that tasks, all possible sequences of scheduler calls and task execution
after the execution of tpl_run_elected() another scheduling event over a given Verification Time Interval (VTI). This requires using
occurs before the elected task starts its execution. For this purpose, models in which time can evolve in order to generate events trig-
a transition synchronized with tpl_run_elected() is used to return gering the Scheduler. Since UPPAAL offers the possibility of using
to the Prio_Check state in order to do the verification again after timed automata, we can use them to model the verification engine.
the re-scheduling. Thus, two main parts are considered:
The second requirement, concerning the idleness, it is checked
when all the elected tasks start their execution. It is performed by activation engine: given a number 𝑛 of tasks, this engine allows
using the synchronization channels end_run_elected[core_id] and to generate all possible scenarios of job activation within the inter-
MicroSecondesInc. This is performed by synchronizing the observer val [1, 𝑉𝑇 𝐼 ] which is specified. All possible tasksets that contains
with the Timer automaton through the MicroSecondesInc? channel at most 𝑛 tasks are verified and activations can occur randomly at
which indicates the beginning task execution. This way, when it is anytime and in any order between 1 and 𝑉𝑇 𝐼 time units. For the
synchronized, the observer checks its requirement based on a test sake of simplicity, two timed automata are used to describe this
related to the Idleness_Check state. behavior:
• activate_once: this template is used to activate at most 𝑛
5.2 Requirements formal specification jobs only one time between 1 and 𝑉𝑇 𝐼 . Figure 7 shows an
Each requirement is formally specified using reachability test on example of activation engine that can activate up to 6 tasks
the Good and Bad states of the corresponding observer. This property (𝑛 = 6). In the initial state, all tasks are in the SUSPENDED
is defined below. state. The time progresses continuously using a clock vari-
able timer_c. When the time starts to run, the automaton is
Definition 5.1 (Reachability). This property checks for a given synchronized with the timer automaton using the channel
state 𝑠 of the model if there exists a path starting at the initial state, MicroSecondsInc?. This synchronization is used to prevent
such that s is eventually reached along that path. the activation of jobs before that the OS starts. Once the
RTNS 2020, June 9–10, 2020, Paris, France K.Boukir, et al.

the activation of multiple jobs for the same task even if the
oldest ones are not yet terminated.
Figure 8 presents an example an automaton that can activate
several jobs for 3 tasks at anytime and in random order.
Some possible activating scenarios using this template are
presented in the following:
scenario 1: only jobs of 𝜏0 are activated in different dates
{𝑡 1, 𝑡 2, ..., 𝑡𝑚𝑎𝑥 } such that {1 ≤ 𝑡 1 < 𝑡 1 < ... < 𝑡𝑚𝑎𝑥 ≤
𝑉𝑇 𝐼 }.
scenario 2: no job is activated which can be a possible sce-
nario as well.
execution engine: it’s a task model which is introduced to de-
scribe an indeterministic task behavior. Our purpose is not to pro-
vide a model that accurately describes how a task runs during its
execution, but to develop a model that covers as many cases of exe-
cution scenarios as possible. To this end, each task is abstracted by a
timed automaton that gathers all the states in which a basic task can
be (cf. Fig. 9). In the Main state of the automaton, a task can either
be SUSPENDED, READY or RUNNING. When it is activated by one of the
Figure 7: activate_once template
previous activation engines (Fig. 7, 8), the task is considered READY
but stays in the Main state. When it is selected for execution by the
Scheduler, the task becomes RUNNING and the function IS_RUNNING()
returns true. The execution time of the task is indeterministic, the
model handles all the possible cases where a task can be executed
between 1 and VTI time units as long as it is in the Main state. For
termination, the task can finish its execution at any time before
the expiration of VTI. To do so, it goes to the Termination state
using a transition which is guarded by the IS_RUNNING() function.
This guard is used to avoid calling the TerminateTask automaton
while the task is not running or preempted. The execution can be
performed in a best case scenario in which a task runs for zero time
units and the worst case scenario in which it runs for VTI time
units. All scenarios in between are treated as well. This widens the
scope of verification and allows multiple task configurations to be
Figure 8: activate_several_jobs template verified.

time starts flowing, the automaton moves to the Main state

and can choose or not to take any transition to activate any
task at any time as long as the VTI date is not reached. This
is carried out using the invariant timer_c <= VTI that also
allows the automaton to end the scenario when the verifi-
cation time is expired. We present some possible scenarios
that are covered by this automaton:
scenario 1: 𝑛 tasks where 𝑛 <= 6 (since the automaton can Figure 9: Task model template
activate at most 6 tasks): 𝜏𝑖 / 𝑖 ∈ {0, 1, ..., 𝑛−1} are activated
simultaneously at 𝑡 = 1.
scenario 2: 𝑛 tasks where 𝑛 <= 6: 𝜏𝑖 are activated respec-
tively at different times {𝑡 1, 𝑡 2, ..., 𝑡𝑛 } such that {1 ≤ 𝑡 1 < 5.4 Verification scenarios
𝑡 2 < ... < 𝑡𝑛 ≤ 𝑉𝑇 𝐼 }. Since our goal is to be able to verify the functional correctness of
• activate_several_jobs: This template allows the activation the implementation, task configurations are chosen in such a way
of several jobs of the same task while previous jobs are not that they provide scenarios with the respect to the requirements
yet terminated. It follows the same principle as the previous presented in 4.2. In this part, we present examples of activation
template. Activations can occur at anytime and in any order and execution scenarios used for verification. We consider that
as long as the VTI is not reached. This is mainly used to the tasks have to compete for execution on 2 cores. Note that the
check the properties of the PendingJobList since it allows value of VTI chosen for each scenario corresponds to the value
Requirement specification and model-checking of a RT scheduler implementation RTNS 2020, June 9–10, 2020, Paris, France

required to conclude that the verified component is behaving cor- (5) for the Context Switch Manager: the consideration of a single
rectly with the respect to its requirements. For example, to verify task in a 𝑉𝑇 𝐼 greater than its maximum activation count can
that the scheduler is called when an activation occurs, we just need be relevant to check the context switching requirement after
a task to be activated and check the corresponding property in the the activation and the termination of the task.
component observer in question. Such a task can be activated using
the activate_once engine and a VTI of one time unit is sufficient to 6 DETECTED SCHEDULING ERRORS
observe the activation. The same logic is used for every requirement To apply our verification approach, the scenarios described above
to chose the values of VTI in the following. were tested on the complete OS model. Reachability tests on the
(1) for the Task Manager: checking its requirements can be suf- observers bad states were carried out to check the requirements
ficient by specifying an application with one task that can introduced in Section 4.2 (E <> Observer.Bad). If this property holds,
run in an interval allowing multiple activations of it using it means that the expected behavior of the corresponding compo-
the activate_several_jobs template (Fig. 8). Activating sev- nent is not achieved. The counterexample sequence execution is
eral jobs of a task before terminating the old one allows generated along with the sequence variable to indicate the branch
the checking of requirements related to the activation count that led the system to the Bad state. This check allowed us to find
incrementation/decrementation, the switching between the out some implementation errors in the scheduling perimeter source
ReadyList and the PendingJobList and also if the Scheduler code which are mainly the consequence of Trampoline’s transition
is called for every scheduling event (activation/termination). from partitioned to global scheduling. These errors were detected
Since the automaton allows job activations that are sepa- by analyzing the generated counterexample scenarios.
rated by one time unit minimum, it is necessary to have
1. In the initial version of Trampoline, in which partitioned
𝑉𝑇 𝐼 > 𝑚𝑎𝑥_𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑖𝑜𝑛_𝑐𝑜𝑢𝑛𝑡 + 1 in order to consider the
scheduling was supported, each task is statically assigned to a
case of activating all the jobs of the task.
single core for its execution. Thus, if a task 𝜏𝑖 is preempted, there
(2) for the Time Manager: the purpose is to calculate and com-
is no possibility that it will be selected to be executed on another
pare successfully deadlines of different tasks. Thus, the VTI
core. Therefore, in the initial implementation of the Trampoline’s
to verify the requirements of the Time Manager must be
scheduler, a preempted task is only put back into the ReadyList at
higher than the maximum value that a deadline can take
the end of context switching.
in a cycle. If an absolute deadline is represented on 𝑛 bits,
When moving to global scheduling, Some call sequences of OS
the maximum value that it can have is 𝑃 = 2𝑛 − 1. Thus, it
functions has been preserved which conducted to the following
is possible to consider a VTI of 8 time units for deadlines
error. A task 𝜏𝑖 which is preempted on a core 𝐶𝑖 , might have a
that are represented on 3 bits in order to exceed the timer’s
higher priority than a task 𝜏 𝑗 running on a core 𝐶 𝑗 . However, if
period and cover the case of two deadlines represented on
𝜏𝑖 is only put back in the ReadyList at the context switching level
two different cycles. An example of a task configuration
(after the scheduling), the Scheduler can not take it into account
can be: 2 tasks to be executed on 2 processors with activa-
while taking its decision. As a result, the running task 𝜏 𝑗 will have
tions generated by the activate_once template. A possible
a lower priority than the ready task 𝜏𝑖 .
scenario of this task configuration can be the activation of
the two tasks at the same time. This necessarily leads to a Counterexample scenario. The aforementioned error was de-
deadline calculation first and comparison since the 2 tasks tected under the scenario intended to verify the Scheduler’s require-
are compared before being stored in the ReadyList. ments (cf. 5.4): 3 tasks: 𝜏0 , 𝜏1 , and 𝜏2 to be executed on 2 cores that
(3) for the Task List Manager: to check the heap property for the are denoted 𝐶 0 and 𝐶 1 . Each task 𝜏𝑖 has relative deadline denoted by
ReadyList, 2 tasks are needed. To cover the case of having 𝐷𝑖 . The activation is performed using the activate_several_jobs
two jobs linked in the same heap node, we consider that 2 template since each task 𝜏𝑖 have a maximum activation count equal
tasks have the same relative deadline. In order to check the to 2. The considered VTI is 7 time units. The counterexample sce-
PendingJobLists we consider that the tasks have a maximum nario that was generated by UPPAAL model-checker is described
activation count of 3 which covers the case of having one below:
active job per task in the ReadyList and 2 pending jobs per • at 𝑡 1 , 𝐽11 and 𝐽21 are released. Their absolute deadlines are
task in their PendingJobLists. calculated: 𝑑 11 = 𝐷 1 + 𝑡 1 and 𝑑 21 = 𝐷 2 + 𝑡 1 such that 𝑑 11 < 𝑑 21 .
(4) for the Scheduler: considering that the execution is carried Thus, 𝐽11 is scheduled to be executed on core 𝐶 0 and 𝐽21 on
out on two cores, at least two running tasks are needed. In core 𝐶 1 .
order to check the priority requirement, a third task with dif- • at 𝑡 2 > 𝑡 1 , 𝐽01 is released, its absolute deadline is calculated:
ferent deadline must be considered to compare with the other
𝑑 01 = 𝐷 0 + 𝑡 2 such that 𝑑 01 < 𝑑 11 < 𝑑 21 . 𝐽01 is put in the
two tasks. The requirement asserts that a running job shall
ReadyList and the Scheduler is called. Since 𝑑 01 < 𝑑 11 , the
have a lower deadline that any other job in the ReadyList
or any of the PendingJobList. Thus, pending jobs must be Scheduler preempts 𝐽11 and extracts 𝐽01 from the ReadyList to
considered for the three tasks. In that case, an application be executed on core 𝐶 0 .
composed of 3 tasks with a maximum activation count of • after the context switching, 𝐽11 is put back in the ReadyList.
two each is proposed. This scenario violates the requirement of the priority according
to G-EDF policy. At 𝑡 2 in the execution, job 𝐽11 is stored in the
RTNS 2020, June 9–10, 2020, Paris, France K.Boukir, et al.

Component Scenario Number of explored states Runtime (ms) Memory (Kibytes)

Task Manager - one task 10 965 1 640 63 780
- max activation count = 2
- VTI = 3
Time Manager - 2 tasks 178 691 012 3.0733e+07 33 650 960
- max activation count = 1
- VTI = 8
Task List Manager - 2 tasks 13 451 183 2.42331e+06 1 537 936
- max activation count = 3
- VTI = 7
Scheduler - 3 tasks 1 362 177 190 1.78361e+08 157 922 424
- max activation count = 2
- VTI = 7
Context Switch Man- - one task 6 285 900 63 368
ager - max activation count = 1
- VTI = 2
Table 2: Verification performances

ReadyList while 𝐽𝑖2 which has a lower priority is running on core Note that in addition to the requirements presented in Section
𝐶1 . 4.2, the complete model was also previously checked using the
property "AG not deadlock" in order to conduct our approach on a
2. As mentioned before, in the partitioned scheduling version
deadlock free system. This property means that deadlock does not
of Trampoline, a task is statically assigned to a core. The identifier
occur for any path of the model, globally.
of this core is initialized in an API layer function that does not
belong to the scheduling perimeter. In some specific cases, such
7 CONCLUSION
as the case of AUTOSTART tasks 2 , a macro of the Context Switch
Manager is called through the API aforementioned function taking We proposed a formal method to verify the implementation of
the wrong identifier of the core and ignoring the global scheduling scheduling policies based on model-checking. The approach was
decision. This leads to two possible situations where the G-EDF tested on an implementation of G-EDF scheduler within Trampo-
decision is not respected: (i) the first one involves executing a task line. To do so, a first step of modeling Trampoline’s components
on a core other than the one indicated by the G-EDF scheduler; (ii) that are involved in the scheduling decision was conducted. Models
The second, which is the most serious, is to execute a non-priority abstracting the functioning of these components were elaborated
task according to EDF on the core saved by the API function. using Extended Finite Automata and integrated to an existing model
of the OS. The variables, the actions and the conditions manipulated
Counterexample scenario. This error was detected for the pre- in the models are those present in the source code of Trampoline’s
viously presented scenario of the Scheduler verification, but also components. Thus, these models are very close to the actual source
under a scenario intended to verify the Context Switch Manager. code due to the similarity between the semantics of C language and
3. Other minor errors were also detected using our scenarios: UPPAAL language which makes the verification on those proposed
(i) saving the context of a terminating task by calling the wrong models reliable. The elaborated models were combined with a timer
Context Switch Manager function; (ii) request loading the context of models that abstracts the time progress in the OS to form a com-
a newly activated task which is a consequence of the previous error plete model (OS model + timer). The second step was to establish
; (iii) not updating the size of the PendingJobList after removing a requirements that are sufficient to verify on the elaborated models.
pending job. These requirements were defined according to the expected behav-
This approach allowed us to fix the found :errors in the imple- ior of the scheduler. They are used in observers that are inserted
mented scheduler and ensure its correctness. Due to verification in parallel with the complete model to observe its behavior during
engines, several non-deterministic scenarios of task activation and the execution. The execution of the model was stimulated using
termination were tested in the model. Throughout the development verification engines which provide non-deterministic scenarios of
of this experiment some limitations were encountered. One notable activation and termination of jobs. Therefore, the scenarios that are
issue is the exponential growth of state space during the execution able to trigger the scheduler in accordance with the requirement
which limits the interval 𝑉𝑇 𝐼 during which the verification can to be checked were proposed. This process allowed us to identify
be conducted. Still, thanks to the scenarios discussed in Section some implementation errors and fix them. So far, the proposed
5.4, the requirements were successfully verified. Table 2 shows the approach showed promising results for the given scenarios. Some
verification performances of the approach using a machine of 128 constraints were noted, namely the combinatorial explosion of the
Mbytes of memory and 282428 MHz of CPU. state space beyond a certain verification time since most formal
methods have this property. In order to remedy this problem, our
model is abstracted as much as possible. The model has only 2 clock
2 Tasks that should start automatically and synchronously with the OS start. variables for time progression, the path interleaving is avoided
Requirement specification and model-checking of a RT scheduler implementation RTNS 2020, June 9–10, 2020, Paris, France

using synchronization channels in all automata and observers con- [19] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock,
tain only Committed states. A next step of this work will be to Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael
Norrish, et al. 2009. seL4: Formal verification of an OS kernel. In Proceedings of
demonstrate that the conducted tests are sufficient to validate the the ACM SIGOPS 22nd symposium on Operating systems principles. ACM, 207–220.
functional correctness of the G-EDF implementation. Furthermore, [20] Peng Li, Binoy Ravindran, Syed Suhaib, and Shahrooz Feizabadi. 2004. A formally
verified application-level framework for real-time scheduling on posix real-time
other techniques for model abstraction to limit the explosion of the operating systems. IEEE Transactions on Software Engineering 30, 9 (2004), 613–
state space may also be studied. 629.
This work proposed an analysis of feasibility of this formal ver- [21] Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle/HOL:
a proof assistant for higher-order logic. Vol. 2283. Springer Science & Business
ification approach for schedulers implementation. Since it shows Media.
promising results, model-checking can be engineered and applied [22] Evidence Srl. [n. d.]. Erika enterprise rtos. URL: http://www.evidence.eu.com ([n.
for the implementation of other sophisticated scheduling policies. d.]).
[23] Kabland Toussaint Gautier Tigori, Jean-Luc Béchennec, Sébastien Faucou, and
Accordingly, we intend to pursue this work and extend it to some Olivier Henri Roux. 2017. Formal Model-Based Synthesis of Application-Specific
of these policies. Static RTOS. ACM Transactions on Embedded Computing Systems (TECS) 16, 4
(2017), 97.
[24] Libor Waszniowski, Jan Krákora, and Zdeněk Hanzálek. 2009. Case study on
REFERENCES distributed and fault tolerant system modeling based on timed automata. Journal
[1] Karine Altisen, Gregor Gößler, and Joseph Sifakis. 2002. Scheduler modeling of Systems and Software 82, 10 (2009), 1678–1694.
based on the controller synthesis paradigm. Real-Time Systems 23, 1-2 (2002),
55–84.
[2] Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli,
Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y Vardi, and Lenore D
Zuck. 2005. Formal verification of backward compatibility of microcode. In
International Conference on Computer Aided Verification. Springer, 185–198.
[3] Theodore P Baker. 2010. What to make of multicore processors for reliable
real-time systems?. In International Conference on Reliable Software Technologies.
Springer, 1–18.
[4] Luciano Porto Barreto and Gilles Muller. 2001. Bossa: a DSL framework for
application-specific scheduling policies. Ph.D. Dissertation. INRIA.
[5] Jean-Luc Béchennec, Mikael Briday, Sébastien Faucou, and Yvon Trinquet. 2006.
Trampoline an open source implementation of the OSEK/VDX RTOS specification.
In Emerging Technologies and Factory Automation, 2006. ETFA’06. IEEE Conference
on. IEEE, 62–69.
[6] Jean-Luc Béchennec, Olivier H. Roux, and Toussaint Tigori. 2018. Formal Model-
Based Conformance Verification of an OSEK/VDX Compliant RTOS. In CODIt
2018-5th International Conference on Control, Decision and Information Technolo-
gies.
[7] Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi.
1996. UPPAAL—a tool suite for automatic verification of real-time systems.
Hybrid Systems III (1996), 232–243.
[8] Jean-Paul Bodeveix, Mamoun Filali, Julia L Lawall, and Gilles Muller. 2007. Auto-
matic verification of bossa scheduler properties. Electronic Notes in Theoretical
Computer Science 185 (2007), 17–32.
[9] Khaoula Boukir, Jean-Luc Béchennec, and Anne-Marie Déplanche. 2017. Reducing
the gap between theory and practice: towards A Proven Implementation of Global
EDF in Trampoline. JRWRTC 2017 (2017), 9.
[10] Khaoula Boukir, Jean-Luc Béchennec, and Anne-Marie Déplanche. 2018. Formal
approach for a verified implementation of Global EDF in Trampoline. In Pro-
ceedings of the 26th International Conference on Real-Time Networks and Systems.
ACM, 83–92.
[11] John M Calandrino, Hennadiy Leontyev, Aaron Block, UmaMaheswari C Devi,
and James H Anderson. 2006. LITMUSRT : A Testbed for Empirically Comparing
Real-Time Multiprocessor Schedulers. In Real-Time Systems Symposium, 2006.
RTSS’06. 27th IEEE International. IEEE, 111–126.
[12] Alessio Carlini and Giorgio C Buttazzo. 2003. An efficient time representation
for real-time embedded systems. In Proceedings of the 2003 ACM symposium on
Applied computing. ACM, 705–712.
[13] Felipe Cerqueira, Felix Stutz, and Björn B Brandenburg. 2016. PROSA: A case for
readable mechanized schedulability analysis. In 2016 28th Euromicro Conference
on Real-Time Systems (ECRTS). IEEE, 273–284.
[14] Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Benjamin Werner, and
Christine Paulin-Mohring. 1991. The COQ proof assistant user’s guide: version 5.6.
Ph.D. Dissertation. INRIA.
[15] Dario Faggioli, Michael Trimarchi, Fabio Checconi, Marko Bertogna, and Antonio
Mancina. 2009. An implementation of the earliest deadline first algorithm in
Linux. In Proceedings of the 2009 ACM symposium on Applied Computing. ACM,
1984–1989.
[16] Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. 2006. Schedu-
lability analysis of fixed-priority systems using timed automata. Theoretical
Computer Science 354, 2 (2006), 301–317.
[17] Limor Fix. 2008. Fifteen years of formal property verification in Intel. In 25 Years
of Model Checking. Springer, 139–144.
[18] Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, and David Costanzo.
2011. CertiKOS: a certified kernel for secure cloud computing. In Proceedings of
the Second Asia-Pacific Workshop on Systems. ACM, 3.