validation.aadl 4.58 KB
Newer Older
jhugues's avatar
jhugues committed
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
package validation
public
  with Data_Model;
  with Deployment;

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

subprogram spg_printer1
properties
  source_language => C;
  source_name     => "print_lot_of_stuff";
  source_text     => ("printer.c");
end spg_printer1;

subprogram spg_printer2
properties
  source_language => C;
  source_name     => "print_too_many_stuff";
  source_text     => ("printer.c");
end spg_printer2;

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

thread thr_printer1
end thr_printer1;

thread implementation thr_printer1.i
32
calls
jhugues's avatar
jhugues committed
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
mycalls: {
  P_Spg : subprogram spg_printer1;
};
properties
  Dispatch_Protocol                  => Periodic;
  Period                             => 1000 Ms;
  Compute_Execution_time             => 0 ms .. 3 ms;
  Deadline                           => 1000 ms;
  Priority                           => 2;
  Source_Data_Size                   => 4 Bytes;
  Source_Code_Size                   => 2 Bytes;
  Source_Stack_Size                  => 2 Bytes;
end thr_printer1.i;

thread thr_printer2
end thr_printer2;

thread implementation thr_printer2.i
51
calls
jhugues's avatar
jhugues committed
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
mycalls: {
  Q_Spg : subprogram spg_printer2;
};
properties
  Dispatch_Protocol                  => Sporadic;
  Period                             => 10 Ms;
  deadline                           => 10 Ms;
  Compute_Execution_time             => 0 ms .. 3 ms;
  Priority                           => 1;
  Source_Data_Size                   => 4 Bytes;
  Source_Code_Size                   => 2 Bytes;
  Source_Stack_Size                  => 2 Bytes;
end thr_printer2.i;

processor native
properties
  Deployment::Execution_Platform => native;
end native;

processor implementation native.i
72
properties
jhugues's avatar
jhugues committed
73
74
   Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
   Priority_Range => 0 .. 255;
75
76
   Scheduler_Quantum => 0 Ms;
   Preemptive_Scheduler => true;
jhugues's avatar
jhugues committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
end native.i;

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

process prs_printer
end prs_printer;

process implementation prs_printer.i
subcomponents
  p1        : thread validation::thr_printer1.i;
  p2        : thread validation::thr_printer2.i;
properties
   Source_Data_Size => 4 Bytes;
   Source_Code_Size => 2 Bytes;
end prs_printer.i;

memory ram
end ram;

memory implementation ram.i
properties
   Word_Size => 8 bits;
101
   Byte_Count => 1;
jhugues's avatar
jhugues committed
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
end ram.i;

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

system mysystem
end mysystem;

system implementation mysystem.local
subcomponents
  Node   : process prs_printer.i;
  CPU    : processor native.i;
  RAM    : memory ram.i;
properties
  actual_processor_binding => (reference (CPU)) applies to Node;
  actual_memory_binding    => (reference (RAM)) applies to Node;
annex real_specification {**
   theorem Contains_Memories
      foreach s in system_set do
         mainmem        := {y in Memory_Set | is_subcomponent_of (y, s)};

         check ( (Cardinal (mainmem) > 0) and
125
                 (Property_Exists (mainmem, "Byte_Count"))
jhugues's avatar
jhugues committed
126
127
128
129
130
131
132
133
               );
   end Contains_Memories;
**};
annex real_specification {**
   theorem Check_Memory_And_Process_Mem
      foreach m in memory_set do
         prs            := {x in Process_Set | is_bound_to (m, x)};

134
         check ( ((Get_Property_Value (m, "Word_Size")) * (Get_Property_Value (m, "Byte_Count"))) >
jhugues's avatar
jhugues committed
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
                 ((sum(Get_Property_Value (prs, "Source_Data_Size")))+
                  (sum(Get_Property_Value (prs, "Source_Code_Size"))))
               );
   end Check_Memory_And_Process_Mem;
**};
annex real_specification {**
   theorem Check_Thread_And_Process_Mem
      foreach p in process_set do
         thrs           := {y in Thread_Set | is_subcomponent_of (y, p)};

         check ( (
                  (Sum (Get_Property_Value (thrs, "Source_Data_Size")))+
                  (Sum (Get_Property_Value (thrs, "Source_Code_Size")))+
                  (Sum (Get_Property_Value (thrs, "Source_Stack_Size")))
                 )
               <
                 ((Get_Property_Value (p, "Source_Data_Size"))+
                  (Get_Property_Value (p, "Source_Code_Size")))
               );
   end Check_Thread_And_Process_Mem;
**};
annex real_specification {**
   theorem Check_Processor_Compliance
      foreach p in processor_set do
         prs            := {x in Process_Set | is_bound_to (x, p)};
         thrs           := {y in Thread_Set  | is_subcomponent_of (y, prs)};

         check ( (Min(Get_Property_Value (thrs, "Priority")) > First (Get_Property_Value (p, "Priority_Range"))) and
                (Max (Get_Property_Value (thrs, "Priority")) < Last (Get_Property_Value (p, "Priority_Range"))));

   end Check_Processor_Compliance;
**};


end mysystem.local;

end validation;