property set Deployment is Allowed_Transport_APIs : type enumeration (BSD_Sockets, SpaceWire); Transport_API : Deployment::Allowed_Transport_APIs applies to (bus); Location : aadlstring applies to (processor, device); Port_Number : aadlinteger applies to (process, device); Process_ID : aadlinteger applies to (process, device); Channel_Address : aadlinteger applies to (process, device); Protocol_Type : type enumeration (iiop, diop); Protocol : Deployment::Protocol_Type applies to (system); Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS); Execution_Platform : Deployment::Allowed_Execution_Platform applies to (processor); Priority_Type : type aadlinteger 0 .. 255; Priority : Deployment::Priority_Type applies to (data, thread); Driver_Name : aadlstring applies to (device); Configuration : aadlstring applies to (device); end Deployment; package RMAAadl public with Deployment; subprogram Hello_Spg_1 properties source_language => Ada95; source_name => "Hello.Hello_Spg_1"; end Hello_Spg_1; subprogram Hello_Spg_2 properties source_language => Ada95; source_name => "Hello.Hello_Spg_2"; end Hello_Spg_2; thread Task end Task; thread implementation Task.impl_1 calls MyCalls : {P_Spg : subprogram Hello_Spg_1;} ; properties Dispatch_Protocol => periodic; Period => 1000 ms; Compute_Execution_time => 0 ms .. 3 ms; Deadline => 1000 ms; Source_Stack_Size => 13952 Bytes; end Task.impl_1; thread implementation Task.impl_2 calls MyCall : {P_Spg : subprogram Hello_Spg_2;} ; properties Dispatch_Protocol => periodic; Period => 500 ms; Compute_Execution_time => 0 ms .. 3 ms; Deadline => 500 ms; Source_Stack_Size => 13952 Bytes; end Task.impl_2; processor cpurm properties Deployment::Execution_Platform => ERC32_ORK; end cpurm; processor implementation cpurm.impl properties Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol); end cpurm.impl; process node_a end node_a; process implementation node_a.impl subcomponents Task1 : thread Task.impl_1; Task2 : thread Task.impl_2; annex real_specification {** -- integer_and_binaries_operators theorem integer_and_binaries_operators foreach e in processor_set do check (((((2 ** 2) = 4) and ((2 + 4) = (2 * 3))) or ((2 - 1) >= (4 / 2)))); end integer_and_binaries_operators; **}; end node_a.impl; system rma end rma; system implementation rma.ERC32 subcomponents node_a : process node_a.impl; cpu_rm : processor cpurm.impl; properties Actual_Processor_Binding => (reference ( cpu_rm )) applies to node_a; end rma.ERC32; end RMAAadl;