Abstract
This paper presents a method based on formal specifications for building
robust real-time microkernels.
Temporal logic is used to specih the functional and temporal properties
of real-time kernels with respect to
their main services (e.g., scheduling, time, synchronization, and clock
interrupts). As an example of
a synchronization mechanism, the specification of the Priority Ceiling
Protocol is provided. The objective is to
verify kernel properties at runtime in order to improve the internal
kernel’s
detection mechanisms and
complement their weaknesses. The core of this paper is a complete description
of the temporal logic formulas corresponding to real-time kernel specifications.
The formulas developed in this paper are the basis for the implementation
of fault containment wrappers. The combination of COTS microkernels and
wrappers leak to the notion of robust microkernels. The provided case
study illustrates the approach on top of an instance of the Chorus microkernel.
Keywords: Formal specification, operating
system kernels, real-time systems, synchronisation, temporal logic.
|