Title :
A formal model of a run-time kernel for Ravenscar
Author :
Lundqvist, Kristina ; Asplund, Lars
Author_Institution :
Inf. Technol., Uppsala Univ., Sweden
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;
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
DOI :
10.1109/RTCSA.1999.811307
