Profil Ravenscar
Le profil Ravenscar est un sous-ensemble du langage Ada dédié aux systèmes temps réel nécessitant une grande sûreté de fonctionnement. Il ne restreint que les fonctionnalités liées au parallélisme.
L'idée est de permettre de prouver formellement les propriétés temps-réel des programmes écrits selon ce profil. Le profil Ravenscar, en interdisant un certain nombre de caractéristiques du langage Ada, permet de rendre applicables les outils de preuve de programme.
Les restrictions apportées permettent également de réaliser des exécutifs plus simples, et donc eux-mêmes certifiables.
Ce profil a aussi été appliqué à la spécification temps réel RTSJ du langage Java[1].
Restrictions apportées par le profil
Le profil Ravenscar est maintenant intégré à la norme Ada (2005). Il suffit d'appliquer la directive de compilation suivante:
pragma Profile (Ravenscar);
Ce profil est Ă©quivalent Ă l'ensemble de pragmas de configuration suivants:
pragma Task_Dispatching_Policy (FIFO_Within_Priorities);
pragma Locking_Policy (Ceiling_Locking);
pragma Detect_Blocking;
pragma Restrictions (
No_Abort_Statements,
No_Dynamic_Attachment,
No_Dynamic_Priorities,
No_Implicit_Heap_Allocations,
No_Local_Protected_Objects,
No_Local_Timing_Events,
No_Protected_Type_Allocators,
No_Relative_Delay,
No_Requeue_Statements,
No_Select_Statements,
No_Specific_Termination_Handlers,
No_Task_Allocators,
No_Task_Hierarchy,
No_Task_Termination,
Simple_Barriers,
Max_Entry_Queue_Length => 1,
Max_Protected_Entries => 1,
Max_Task_Entries => 0,
No_Dependence => Ada.Asynchronous_Task_Control,
No_Dependence => Ada.Calendar,
No_Dependence => Ada.Execution_Time.Group_Budget,
No_Dependence => Ada.Execution_Time.Timers,
No_Dependence => Ada.Task_Attributes);
Références
- Alan Burns « The Ravenscar Profile » dans ACM SIGAda Ada Letters , vol XIX issue= 4 pages= 49-52 [lire en ligne]
- Alan Burns, Brian Dobbing and Tullio Vardanega « Guide for the use of the Ada Ravenscar Profile in high integrity systems » dans ACM SIGAda Ada Letters, , vol.XXIV issue= 2 pages= 1-74 [lire en ligne]
- AI95-00249 — Ravenscar profile for high-integrity systems
Notes
- J. Kwon, A. Wellings, and S. King, « Ravenscar-Java: A High Integrity Profile for Real-Time Java», York Technical Report (YCS 342), Department of Computer Science, University of York, 2002, [lire en ligne]