A FORMALLY BASED HARD REAL-TIME KERNEL

Authors
BRADLEY S HENDERSON W KENDALL D ROBSON A
Citation
S. Bradley et al., A FORMALLY BASED HARD REAL-TIME KERNEL, Microprocessors and microsystems, 18(9), 1994, pp. 513-521
Citations number
17
Categorie Soggetti
Computer Sciences","Engineering, Eletrical & Electronic","Computer Science Hardware & Architecture","Computer Science Theory & Methods
Journal title
Microprocessors and microsystems → ACNP
ISSN journal
01419331
Volume
18
Issue
9
Year of publication
1994
Pages
513 - 521
Database
ISI
SICI code
0141-9331(1994)18:9<513:AFBHRK>2.0.ZU;2-R
Abstract
In order to demonstrably satisfy hard real-time deadlines, a system mu st be predictable, and in particular the kernel must be predictable. I n this paper we present and analyse a predictable kernel related to AO RTA, a formal design language for hard real-time systems. The features of the kernel allow AORTA designs to be verifiably and semi-automatic ally implemented, and enable verified guarantees to be given about the real-time behaviour of the system.