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, VXWORKS); 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 {** -- check_expression_max theorem check_expression_max foreach e in process_set do new_set(e) := { x in thread_set | is_subcomponent_of(x, e)}; check ((max(get_property_value(New_Set, "period")) = 1000.0)); end check_expression_max; -- check_expression_sum theorem check_expression_sum foreach e in process_set do new_set(e) := { x in thread_set | is_subcomponent_of(x, e)}; check ((sum(get_property_value(New_Set, "period")) = 1500.0)); end check_expression_sum; -- check_expression_not theorem check_expression_not foreach e in processor_set do check (not (2 = 3)); end check_expression_not; -- check_expression_complex theorem check_expression_complex foreach e in processor_set do test_set := { p in process_set | is_bound_to(p, e)}; check ((((2 = 3) or (2 = 2)) and (cardinal(Test_Set) > 0))); end check_expression_complex; -- check_expression_range theorem check_expression_range foreach e in thread_set do check ((last(get_property_value(e, "compute_execution_time")) > first(get_property_value(e, "compute_execution_time")))); end check_expression_range; **}; 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;