test_real_exec_04.aadl 4.84 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
package Test4_REAL
public

-----------------
-- Subprograms --
-----------------

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;

-------------
-- Threads --
-------------

thread Task
end Task;

thread implementation Task.impl_1
calls
   MyCalls : {
      P_Spg : subprogram Hello_Spg_1;
   };
properties
   Dispatch_Protocol                  => periodic;
   Period                             => 1000ms;
   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                             => 500ms;
   Compute_Execution_time             => 0 ms .. 3 ms;
   Deadline                           => 500 ms;
   Source_Stack_Size                  => 13952 Bytes;
end Task.impl_2;

---------------
-- Processor --
---------------

processor cpurm
end cpurm;

processor implementation cpurm.impl
properties 
   Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
end cpurm.impl;

---------------
-- Processes --
---------------

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 {**

--  tests the Max verification function with the Get_Property_Value function 
--  access

theorem check_expression_max

foreach e in Process_Set do

   New_Set(e) := {x in Thread_Set | Is_Subcomponent_Of (x, e)};

88
   check (Max (Get_Property_Value (New_Set, "Period")) = 1000000000000.0);
89 90 91 92 93 94 95 96 97 98 99
end;

--  tests the Sum verification function with the Get_Property_Value function 
--  access

theorem  check_expression_sum

foreach e in Process_Set do

   New_Set(e) := {x in Thread_Set | Is_Subcomponent_Of (x, e)};

100
   check (Sum (Get_Property_Value (New_Set, "Period")) = 1500000000000.0);
101 102 103 104 105
end;

--  tests the Product verification function with the Get_Property_Value 
--  function access

106
--  XXX this test has been disabled, as it causes an overflow at runtime
107

108
-- theorem  check_expression_product
109

110
-- foreach e in Process_Set do
111

112 113 114 115
--    New_Set(e) := {x in Thread_Set | Is_Subcomponent_Of (x, e)};

--    check (Product (Get_Property_Value (New_Set, "Period")) = 500000.0);
-- end;
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242


--  tests 'not' operator on check expressions

theorem check_expression_not

foreach e in Processor_Set do

  check (not (2 = 3));
end;

--  tests parsing and interpretation of (complex) check expression when 
--  using verification functions as leaf with implicit priorities (ie. no
--  parenthesis in one sub-expression)


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;

--  tests the 'Last' and 'First' verification functions on range 
--  property values

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;

--  tests LCM (Least Common Multiple) verification function with 
--  lists and integers

theorem check_expression_lcm

  foreach e in System_Set do

    var var_list := list (2, 4, 6);

  check (lcm (2, 4, 6) = 12 and
         lcm (var_list) = 12);

end check_expression_lcm;

--  tests GCD (Greatest Common Divisor) verification function with 
--  lists and integers

theorem check_expression_gcd

  foreach e in System_Set do

    var var_list := list (2, 4, 6);

  check (gcd (2, 4, 6) = 2 and
         gcd (var_list) = 2);

end check_expression_gcd;

--  tests the GCD building with variables

theorem check_expression_gcd_var

  foreach e in System_Set do

    var v1 := 2;
    var v2 := 4;
    var v3 := 6;

    check (lcm (v1, v2, v3) = 12);

end check_expression_gcd_var;

--  test the non_null function

theorem check_expression_non_null

  foreach e in System_Set do

    var v0 := 0;
    var v1 := 42;

  check ((non_null(v0) = 0) and (non_null(v1) = 1));

end check_expression_non_null;


--  Test is_in on sets

theorem check_is_in

  foreach s in process_set do

    set := {t in thread_set | is_subcomponent_of (t, s)};

  check (is_in (set, thread_set));

end check_is_in;

**};
end node_a.impl;

------------
-- System --
------------

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