Perfil Ravenscar

O perfil Ravenscar é um subconjunto da linguagem Ada dedicado a sistemas de tempo real que requerem alta confiabilidade operacional . Ele apenas restringe as funcionalidades relacionadas ao paralelismo .

A ideia é possibilitar a comprovação formal das propriedades em tempo real de programas escritos de acordo com esse perfil. O perfil Ravenscar, ao proibir um certo número de características da linguagem Ada, permite tornar aplicáveis ​​as ferramentas de prova de programas.

As restrições introduzidas também possibilitam a formação de executivos mais simples e, portanto, eles próprios certificáveis.

Este perfil também foi aplicado à especificação RTSJ em tempo real da linguagem Java .

Restrições impostas pelo perfil

O perfil Ravenscar agora está integrado ao padrão Ada (2005). Basta aplicar a seguinte diretiva de compilação:

pragma Profile (Ravenscar);

Este perfil é equivalente ao seguinte conjunto de pragmas de configuração:

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

Referências

Notas

  1. J. Kwon, A. Wellings e S. King, "Ravenscar-Java: A High Integrity Profile for Real-Time Java", York Technical Report (YCS 342), Departamento de Ciência da Computação, University of York, 2002, [ ler online ]