DocumentCode
3395883
Title
A formal model of a run-time kernel for Ravenscar
Author
Lundqvist, Kristina ; Asplund, Lars
Author_Institution
Inf. Technol., Uppsala Univ., Sweden
fYear
1999
fDate
1999
Firstpage
504
Lastpage
507
Abstract
The Ravenscar tasking profile for Ada 95 has been designed to allow implementation of highly safety critical systems in Ada. Ravenscar defines a tasking run-time system with deterministic behaviour and low complexity. We provide a formal model of the primitives provided by Ravenscar including exceptions. This formal model can be used to verify safety properties of applications targeting a Ravenscar-compliant run-time system. As an illustration of this, we model a sample application using all features of Ravenscar and formally verify its correctness using the real-time model checker UPPAAL
Keywords
Ada; formal verification; operating system kernels; real-time systems; Ada 95; Ravenscar; Ravenscar tasking profile; UPPAAL; highly safety critical systems; run-time kernel; tasking run-time system; Application software; Clocks; Delay effects; Information technology; Kernel; Protection; Real time systems; Runtime; Safety; Software maintenance;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Computing Systems and Applications, 1999. RTCSA '99. Sixth International Conference on
Conference_Location
Hong Kong
Print_ISBN
0-7695-0306-3
Type
conf
DOI
10.1109/RTCSA.1999.811307
Filename
811307
Link To Document