A formally based hard real-time kernel

Steven Bradley; William Henderson; David Kendall; Adrian Robson

doi:10.1016/0141-9331(94)90074-4

A formally based hard real-time kernel

Steven Bradley, William Henderson, David Kendall, Adrian Robson

Research output: Contribution to journal › Article › peer-review

6 Citations (Scopus)

Abstract

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 language	English
Pages (from-to)	513-521
Journal	Microprocessors and Microsystems
Volume	18
Issue number	9
DOIs	https://doi.org/10.1016/0141-9331(94)90074-4
Publication status	Published - Nov 1994

Keywords

formal methods
performance prediction
real-time

Access to Document

10.1016/0141-9331(94)90074-4

http://www.sciencedirect.com/science/article/pii/0141933194900744

Cite this

@article{467c169472534668b737f3922afc66ca,

title = "A formally based hard real-time kernel",

abstract = "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.",

keywords = "formal methods, performance prediction, real-time",

author = "Steven Bradley and William Henderson and David Kendall and Adrian Robson",

year = "1994",

month = nov,

doi = "10.1016/0141-9331(94)90074-4",

language = "English",

volume = "18",

pages = "513--521",

journal = "Microprocessors and Microsystems",

issn = "0141-9331",

publisher = "Elsevier",

number = "9",

}

TY - JOUR

T1 - A formally based hard real-time kernel

AU - Bradley, Steven

AU - Henderson, William

AU - Kendall, David

AU - Robson, Adrian

PY - 1994/11

Y1 - 1994/11

N2 - 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.

AB - 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.

KW - formal methods

KW - performance prediction

KW - real-time

U2 - 10.1016/0141-9331(94)90074-4

DO - 10.1016/0141-9331(94)90074-4

M3 - Article

SN - 0141-9331

VL - 18

SP - 513

EP - 521

JO - Microprocessors and Microsystems

JF - Microprocessors and Microsystems

IS - 9

ER -

A formally based hard real-time kernel

Abstract

Keywords

Access to Document

Fingerprint

Cite this