Uppsala University Department of Information Technology

Technical Report 1999-002

A Formal Model of a Ravenscar-Compliant Run-Time Kernel and Application Code

Kristina Lundqvist and Lars Asplund

May 1999

Abstract:
The Ravenscar tasking profile for Ada95 has been designed to allow implementation of 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. 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 and formally verify its correctness using the real-time model checker UPPAAL.

Download BibTeX entry.



Uppsala Universitet