Das Ravenscar Profil ist eine Teilmenge der Ada Sprache gewidmet Echtzeit - Systeme erfordern eine hohe Betriebssicherheit . Es schränkt nur die mit Parallelität verbundenen Funktionen ein .
Die Idee ist es, die Echtzeit- Eigenschaften von Programmen, die gemäß diesem Profil geschrieben wurden , formal zu beweisen . Das Ravenscar-Profil ermöglicht es, indem es eine bestimmte Anzahl von Merkmalen der Ada-Sprache verbietet, die programmfesten Tools anwendbar zu machen.
Die eingeführten Beschränkungen ermöglichen es auch, einfachere Führungskräfte zu schaffen und damit selbst zertifizierbar zu sein.
Dieses Profil wurde auch auf die RTSJ- Echtzeitspezifikation der Java- Sprache angewendet .
Das Ravenscar-Profil ist jetzt in den Ada-Standard (2005) integriert. Wenden Sie einfach die folgende Kompilierungsrichtlinie an:
pragma Profile (Ravenscar);Dieses Profil entspricht den folgenden Konfigurationspragmen:
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);