Formal Analysis of a Real-Time Kernel

Specification

Simon Fowler
Real-Time Systems Research Group
Department of Computer Science
University of York, UK

February 19, 1996

Abstract

The specification of a real-time kernel and the analysis of certain properties of the kernel using the PVS system is presented in this paper. The kernel is designed to provide the minimal functionality to support real-time Ada 95 applications on a uniprocessor system, and the requirements for the kernel are derived from this. The specification consists of an abstract model of the functional and timing requirements for the kernel, and a minimal model of the system that the kernel is designed to support. This system model allows properties such as mutual exclusion to be proved about the kernel with respect to certain assumptions about the system.

1 Introduction

Real-time operating system kernels form a vital component of many modern safety critical systems, and their correctness is essential for the integrity of the entire system. One possible method for assuring this is the application of formal methods to their development. In this report, it is demonstrated how a popular formalism can be applied to the specification and analysis of a simple real-time kernel.

The requirements for the kernel are described in the next section, in terms of the Ada 95 language features that it supports. The kernel itself is then specified, along with a model of the system that it is designed to support. The possibilities for proving various properties of the kernel are then discussed. The remainder of this introduction provides a brief summary of the previous research in this area and explains how the approach presented here differs.

1.1 Previous work

Research has been published on the use of formal methods for the specification of kernels at various levels of abstraction, and the correctness of implementations have been verified with respect to some of these specifications [BW91] [Spi90] [GW94] [Tol95] [FKU94]