Profil Ravenscar

Profil Ravenscar jest podzbiorem Ada języku poświęconej systemów czasu rzeczywistego wymagających wysokiej operacyjną niezawodność . Ogranicza tylko funkcje związane z równoległością .

Chodzi o to, aby umożliwić formalnie udowodnić w czasie rzeczywistym właściwości programów napisanych według tego profilu. Profil Ravenscar, zakazując określonej liczby cech języka Ada, umożliwia zastosowanie narzędzi sprawdzających program.

Wprowadzone ograniczenia umożliwiają również stworzenie prostszej kadry kierowniczej , a tym samym ich certyfikację.

Ten profil został również zastosowany do specyfikacji czasu rzeczywistego RTSJ języka Java .

Ograniczenia nałożone przez profil

Profil Ravenscar jest teraz zintegrowany ze standardem Ada (2005). Po prostu zastosuj następującą dyrektywę kompilacji:

pragma Profile (Ravenscar);

Ten profil jest równoważny z następującym zestawem pragm konfiguracyjnych:

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);

Bibliografia

Uwagi

  1. J. Kwon, A. Wellings i 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, [ czytaj online ]