Verifying, Validating and Monitoring the Open Ravenscar Real Time Kernel1

Business and mission critical real-time systems need to be fully predictable, in order that their behaviour is known before deployment, even in the presence of faults. The Open Ravenscar Real Time Kernel (ORK) is a small size with reduced complexity kernel designed to be used in this type of applications. This kernel was implemented to be fully compliant with the Ravenscar profile, which defines a subset of the tasking features of Ada which can be used to implement a small and reliable kernel. Critical Software has recently conducted an evaluation on this kernel as well as started a new project to provide a monitoring tool for ORK, thus further enhancing the already existing range of hard real-time verification and validation tools. This paper summarizes the objectives and results of the ORK evaluation and presents the main goals and functionalities of the monitoring tool.