Formal specification for building robust real-time microkernels
- 11 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 119-128
- https://doi.org/10.1109/real.2000.896002
Abstract
This paper presents a method based on formal specifications for building robust real-time microkernels. Temporal logic is used to specify 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 leads to the notion of robust microkernels. The provided case study illustrates the approach on top of an instance of the Chorus microkernel.Keywords
This publication has 8 references indexed in Scilit:
- Assessment of COTS microkernels by fault injectionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- MetaKernels and fault containment wrappersPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Formal specification and verification of a real-time kernelPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Design of embedded systems: formal models, validation, and synthesisProceedings of the IEEE, 1997
- Formal analysis of a real-time kernel specificationPublished by Springer Nature ,1996
- Fixed priority pre-emptive scheduling: An historical perspectiveReal-Time Systems, 1995
- Specifying a real-time kernelIEEE Software, 1990
- Priority inheritance protocols: an approach to real-time synchronizationIEEE Transactions on Computers, 1990