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, Native_Compcert, bench, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS); Execution_Platform : Deployment::Allowed_Execution_Platform applies to ( all); Supported_Execution_Platform : list of Deployment::Allowed_Execution_Platform applies to (device); Runtime : type enumeration (PolyORB_HI_C, PolyORB_HI_Ada, POK); Supported_Runtime : Deployment::Runtime applies to ( all); 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); Config : aadlstring applies to (device); ASN1_Module_Name : aadlstring applies to ( all); Help : aadlstring applies to ( all); Version : aadlstring applies to ( all); Configuration_Type : classifier ( data) applies to ( all); 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 {** -- type_issues_1 theorem type_issues_1 foreach e in processor_set do check ((2.0 <> 2.1)); end type_issues_1; -- type_issues_2 theorem type_issues_2 foreach e in processor_set do check (("bla" <> "blo")); end type_issues_2; -- type_issues_3 theorem type_issues_3 foreach e in processor_set do check (((int(2.0) = 2) and (2.0 = float(2)))); end type_issues_3; **}; 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;