A formally based hard real-time kernel

Steven Bradley, William Henderson, David Kendall, Adrian Robson

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)


In order to demonstrably satisfy hard real-time deadlines, a system must be predictable, and in particular the kernel must be predictable. In this paper we present and analyse a predictable kernel related to AORTA, a formal design language for hard real-time systems. The features of the kernel allow AORTA designs to be verifiably and semi-automatically implemented, and enable verified guarantees to be given about the real-time behaviour of the system.
Original languageEnglish
Pages (from-to)513-521
JournalMicroprocessors and Microsystems
Issue number9
Publication statusPublished - Nov 1994


Dive into the research topics of 'A formally based hard real-time kernel'. Together they form a unique fingerprint.

Cite this