@TechReport{	  it:1999-002,
  author	= {Kristina Lundqvist and Lars Asplund},
  title		= {A Formal Model of a Ravenscar-Compliant Run-Time Kernel
		  and Application Code},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {1999},
  number	= {1999-002},
  month		= may,
  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.}
}