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

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