Formal development of a real-time kernel

S Fowler; A Wellings

Formal development of a real-time kernel

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The formal development of a simple real-time operating system kernel is described in this paper. The kernel provides a set of operations that allows a restricted Ada 95 tasking model to be supported, suitable for fixed priority real-time systems. The requirements for the kernel are expressed in terms of the computational model using RTL, and the abstract specification of the kernel is validated against this. The development of an implementation from this specification is then described, with the PVS proof system used to verify each step in the development process.

Original language	English
Title of host publication	18TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS
Place of Publication	LOS ALAMITOS
Publisher	IEEE Computer Society
Pages	220-229
Number of pages	10
ISBN (Print)	0-8186-8269-8
Publication status	Published - 1997
Event	18th IEEE Real-Time Systems Symposium - SAN FRANCISCO Duration: 2 Dec 1997 → 5 Dec 1997

Conference

Conference	18th IEEE Real-Time Systems Symposium
City	SAN FRANCISCO
Period	2/12/97 → 5/12/97

Cite this

@inproceedings{6465693737e04ecba57e8f11ce4705d4,

title = "Formal development of a real-time kernel",

abstract = "The formal development of a simple real-time operating system kernel is described in this paper. The kernel provides a set of operations that allows a restricted Ada 95 tasking model to be supported, suitable for fixed priority real-time systems. The requirements for the kernel are expressed in terms of the computational model using RTL, and the abstract specification of the kernel is validated against this. The development of an implementation from this specification is then described, with the PVS proof system used to verify each step in the development process.",

author = "S Fowler and A Wellings",

year = "1997",

language = "English",

isbn = "0-8186-8269-8",

pages = "220--229",

booktitle = "18TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS",

publisher = "IEEE Computer Society",

address = "United States",

note = "18th IEEE Real-Time Systems Symposium ; Conference date: 02-12-1997 Through 05-12-1997",

}

TY - GEN

T1 - Formal development of a real-time kernel

AU - Fowler, S

AU - Wellings, A

PY - 1997

Y1 - 1997

N2 - The formal development of a simple real-time operating system kernel is described in this paper. The kernel provides a set of operations that allows a restricted Ada 95 tasking model to be supported, suitable for fixed priority real-time systems. The requirements for the kernel are expressed in terms of the computational model using RTL, and the abstract specification of the kernel is validated against this. The development of an implementation from this specification is then described, with the PVS proof system used to verify each step in the development process.

AB - The formal development of a simple real-time operating system kernel is described in this paper. The kernel provides a set of operations that allows a restricted Ada 95 tasking model to be supported, suitable for fixed priority real-time systems. The requirements for the kernel are expressed in terms of the computational model using RTL, and the abstract specification of the kernel is validated against this. The development of an implementation from this specification is then described, with the PVS proof system used to verify each step in the development process.

M3 - Conference contribution

SN - 0-8186-8269-8

SP - 220

EP - 229

BT - 18TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS

PB - IEEE Computer Society

CY - LOS ALAMITOS

T2 - 18th IEEE Real-Time Systems Symposium

Y2 - 2 December 1997 through 5 December 1997

ER -