Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
O
Ocarina
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
2
Issues
2
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
Operations
Operations
Incidents
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
TASTE
Ocarina
Commits
6d33cabb
Commit
6d33cabb
authored
Jul 02, 2016
by
Bechir Zalila
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
* Test cases for LNT backend
(By Hana Mkaouar)
parent
ffe5d888
Changes
13
Hide whitespace changes
Inline
Side-by-side
Showing
13 changed files
with
3062 additions
and
3 deletions
+3062
-3
tests/LNT/FCS/FCS.aadl
tests/LNT/FCS/FCS.aadl
+188
-0
tests/LNT/FCS/FCS.aadl.out
tests/LNT/FCS/FCS.aadl.out
+734
-0
tests/LNT/FCS/MANIFEST
tests/LNT/FCS/MANIFEST
+3
-0
tests/LNT/PC/MANIFEST
tests/LNT/PC/MANIFEST
+3
-0
tests/LNT/PC/producer_consumer.aadl
tests/LNT/PC/producer_consumer.aadl
+140
-0
tests/LNT/PC/producer_consumer.aadl.out
tests/LNT/PC/producer_consumer.aadl.out
+441
-0
tests/LNT/RADAR/MANIFEST
tests/LNT/RADAR/MANIFEST
+3
-0
tests/LNT/RADAR/radar.aadl
tests/LNT/RADAR/radar.aadl
+203
-0
tests/LNT/RADAR/radar.aadl.out
tests/LNT/RADAR/radar.aadl.out
+611
-0
tests/LNT/ROBOT/MANIFEST
tests/LNT/ROBOT/MANIFEST
+3
-0
tests/LNT/ROBOT/robot.aadl
tests/LNT/ROBOT/robot.aadl
+199
-0
tests/LNT/ROBOT/robot.aadl.out
tests/LNT/ROBOT/robot.aadl.out
+529
-0
tests/TestList.mk
tests/TestList.mk
+5
-3
No files found.
tests/LNT/FCS/FCS.aadl
0 → 100644
View file @
6d33cabb
package
FlightControlSystem
public
data
Alpha
end
Alpha
;
thread
NL
--
Navigation
Law
features
pos_c
:
in
event
data
port
Alpha
;
pos_o
:
in
event
data
port
Alpha
;
acc_c
:
out
event
data
port
Alpha
;
properties
Dispatch_Protocol
=>
Periodic
;
Period
=>
120
ms
;
Compute_Execution_Time
=>
0
ms
..
20
ms
;
Deadline
=>
120
ms
;
Priority
=>
2
;
end
NL
;
thread
NF
--
Navigation
Filter
features
pos_i
:
in
event
data
port
Alpha
;
pos_o
:
out
event
data
port
Alpha
;
properties
Dispatch_Protocol
=>
Periodic
;
Period
=>
120
ms
;
Compute_Execution_Time
=>
0
ms
..
10
ms
;
Deadline
=>
120
ms
;
Priority
=>
1
;
end
NF
;
thread
PL
--
Piloting
Law
features
acc_c
:
in
event
data
port
Alpha
;
acc_o
:
in
event
data
port
Alpha
;
angle_c
:
out
event
data
port
Alpha
;
properties
Dispatch_Protocol
=>
Periodic
;
Period
=>
40
ms
;
Compute_Execution_Time
=>
0
ms
..
5
ms
;
Deadline
=>
40
ms
;
Priority
=>
4
;
end
PL
;
thread
PF
--
Piloting
Filter
features
acc_i
:
in
event
data
port
Alpha
;
acc_o
:
out
event
data
port
Alpha
;
properties
Dispatch_Protocol
=>
Periodic
;
Period
=>
40
ms
;
Compute_Execution_Time
=>
0
ms
..
5
ms
;
Deadline
=>
40
ms
;
Priority
=>
3
;
end
PF
;
thread
FL
--
Feddback
Law
features
angle_c
:
in
event
data
port
Alpha
;
angle_o
:
in
event
data
port
Alpha
;
order
:
out
event
data
port
Alpha
;
properties
Dispatch_Protocol
=>
Periodic
;
Period
=>
10
ms
;
Compute_Execution_Time
=>
0
ms
..
2
ms
;
Deadline
=>
10
ms
;
Priority
=>
7
;
end
FL
;
thread
FF
--
Feedback
Filter
features
angle_o
:
out
event
data
port
Alpha
;
angle
:
in
event
data
port
Alpha
;
properties
Dispatch_Protocol
=>
Periodic
;
Period
=>
10
ms
;
Compute_Execution_Time
=>
0
ms
..
1
ms
;
Deadline
=>
10
ms
;
Priority
=>
6
;
end
FF
;
thread
AP
--
Acceleration
Position
Acquisition
features
position
:
in
event
data
port
Alpha
;
acc
:
in
event
data
port
Alpha
;
acc_i
:
out
event
data
port
Alpha
;
pos_i
:
out
event
data
port
Alpha
;
properties
Dispatch_Protocol
=>
Periodic
;
Period
=>
10
ms
;
Compute_Execution_Time
=>
0
ms
..
1
ms
;
Deadline
=>
10
ms
;
Priority
=>
5
;
end
AP
;
processor
cpu
features
i2c
:
requires
bus
access
i2c_bus
;
end
cpu
;
process
node_a
features
angle
:
in
event
data
port
Alpha
;
position
:
in
event
data
port
Alpha
;
acc
:
in
event
data
port
Alpha
;
pos_c
:
in
event
data
port
Alpha
;
order
:
out
event
data
port
Alpha
;
end
node_a
;
process
implementation
node_a
.
impl
subcomponents
FF
:
thread
FF
;
NL
:
thread
NL
;
NF
:
thread
NF
;
PL
:
thread
PL
;
PF
:
thread
PF
;
FL
:
thread
FL
;
AP
:
thread
AP
;
connections
--
Inter
-
thread
communication
V1
:
port
NL
.
acc_c
->
PL
.
acc_c
;
V2
:
port
PL
.
angle_c
->
FL
.
angle_c
;
V3
:
port
NF
.
pos_o
->
NL
.
pos_o
;
V4
:
port
PF
.
acc_o
->
PL
.
acc_o
;
V5
:
port
FF
.
angle_o
->
FL
.
angle_o
;
V6
:
port
AP
.
acc_i
->
PF
.
acc_i
;
V7
:
port
AP
.
pos_i
->
NF
.
pos_i
;
--
Process
/
thread
communication
V8
:
port
pos_c
->
NL
.
pos_c
;
V9
:
port
FL
.
order
->
order
;
V10
:
port
angle
->
FF
.
angle
;
V11
:
port
position
->
AP
.
position
;
V12
:
port
acc
->
AP
.
acc
;
end
node_a
.
impl
;
device
Operator
features
pos_c
:
out
event
data
port
Alpha
;
i2c
:
requires
bus
access
i2c_bus
;
end
Operator
;
device
GPS
features
position
:
out
event
data
port
Alpha
;
i2c
:
requires
bus
access
i2c_bus
;
end
GPS
;
device
IMU
features
angle
:
out
event
data
port
Alpha
;
acc
:
out
event
data
port
Alpha
;
i2c
:
requires
bus
access
i2c_bus
;
end
IMU
;
device
Platform
features
order
:
in
event
data
port
Alpha
;
i2c
:
requires
bus
access
i2c_bus
;
end
Platform
;
bus
I2C_bus
--
I2C
bus
end
I2C_bus
;
system
fcs
end
fcs
;
system
implementation
fcs
.
impl
subcomponents
node_a
:
process
node_a
.
impl
;
cpu_rm
:
processor
cpu
;
operator
:
device
Operator
;
GPS
:
device
GPS
;
IMU
:
device
IMU
;
platform
:
device
Platform
;
i2c
:
bus
i2c_bus
;
connections
V13
:
port
operator
.
pos_c
->
node_a
.
pos_c
{
Actual_Connection_Binding
=>
(
reference
(
i2c
));};
V14
:
port
node_a
.
order
->
platform
.
order
{
Actual_Connection_Binding
=>
(
reference
(
i2c
));};
V15
:
port
GPS
.
position
->
node_a
.
position
{
Actual_Connection_Binding
=>
(
reference
(
i2c
));};
V16
:
port
IMU
.
angle
->
node_a
.
angle
{
Actual_Connection_Binding
=>
(
reference
(
i2c
));};
V17
:
port
IMU
.
acc
->
node_a
.
acc
{
Actual_Connection_Binding
=>
(
reference
(
i2c
));};
V18
:
bus
access
i2c
->
GPS
.
i2c
;
V19
:
bus
access
i2c
->
IMU
.
i2c
;
V20
:
bus
access
i2c
->
platform
.
i2c
;
V21
:
bus
access
i2c
->
cpu_rm
.
i2c
;
properties
Actual_Processor_Binding
=>
(
reference
(
cpu_rm
))
applies
to
node_a
;
end
fcs
.
impl
;
end
FlightControlSystem
;
tests/LNT/FCS/FCS.aadl.out
0 → 100644
View file @
6d33cabb
------------------------------------------
---------- Ocarina LNT Generator ---------
------------------------------------------
FCS.aadl:110:03FCS.aadl:111:03FCS.aadl:112:03FCS.aadl:113:03FCS.aadl:114:03FCS.aadl:115:03FCS.aadl:116:03Begin Thread
Begin Processor
Begin Types
Begin Port
Begin Main
FCS.aadl:73:03 FCS.aadl:9:03 FCS.aadl:10:03 FCS.aadl:22:03 FCS.aadl:34:03 FCS.aadl:35:03 FCS.aadl:47:03 FCS.aadl:59:03 FCS.aadl:60:03 FCS.aadl:84:03 FCS.aadl:85:03 "Main.bcg"= divbranching reduction of "FLIGHTCONTROLSYSTEM_Main.lnt";
property PROPERTY_Deadlock is
deadlock of "Main.bcg";
expected FALSE;
end property;
property Scheduling_Test (ID) is
"Main_$ID.bcg"="Main.bcg"|=
[ true* . "ACTIVATION_$ID !T_Error" ] false;
expected TRUE;
end property;
module FLIGHTCONTROLSYSTEM_Threads (FLIGHTCONTROLSYSTEM_Types) is
process Thread_FF [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_ANGLE_O: LNT_Channel_Data,
AADL_PORT_ANGLE: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin);
AADL_PORT_ANGLE (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ANGLE_O (AADLDATA)
[]
ACTIVATION (T_All);
AADL_PORT_ANGLE (AADLDATA);
AADL_PORT_ANGLE_O (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
process Thread_NL [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_POS_C: LNT_Channel_Data,
AADL_PORT_POS_O: LNT_Channel_Data,
AADL_PORT_ACC_C: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin);
AADL_PORT_POS_C (AADLDATA);
AADL_PORT_POS_O (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ACC_C (AADLDATA)
[]
ACTIVATION (T_All);
AADL_PORT_POS_C (AADLDATA);
AADL_PORT_POS_O (AADLDATA);
AADL_PORT_ACC_C (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
process Thread_NF [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_POS_I: LNT_Channel_Data,
AADL_PORT_POS_O: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin);
AADL_PORT_POS_I (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_POS_O (AADLDATA)
[]
ACTIVATION (T_All);
AADL_PORT_POS_I (AADLDATA);
AADL_PORT_POS_O (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
process Thread_PL [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_ACC_C: LNT_Channel_Data,
AADL_PORT_ACC_O: LNT_Channel_Data,
AADL_PORT_ANGLE_C: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin);
AADL_PORT_ACC_C (AADLDATA);
AADL_PORT_ACC_O (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ANGLE_C (AADLDATA)
[]
ACTIVATION (T_All);
AADL_PORT_ACC_C (AADLDATA);
AADL_PORT_ACC_O (AADLDATA);
AADL_PORT_ANGLE_C (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
process Thread_PF [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_ACC_I: LNT_Channel_Data,
AADL_PORT_ACC_O: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin);
AADL_PORT_ACC_I (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ACC_O (AADLDATA)
[]
ACTIVATION (T_All);
AADL_PORT_ACC_I (AADLDATA);
AADL_PORT_ACC_O (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
process Thread_FL [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_ANGLE_C: LNT_Channel_Data,
AADL_PORT_ANGLE_O: LNT_Channel_Data,
AADL_PORT_ORDER: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin);
AADL_PORT_ANGLE_C (AADLDATA);
AADL_PORT_ANGLE_O (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ORDER (AADLDATA)
[]
ACTIVATION (T_All);
AADL_PORT_ANGLE_C (AADLDATA);
AADL_PORT_ANGLE_O (AADLDATA);
AADL_PORT_ORDER (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
process Thread_AP [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_POSITION: LNT_Channel_Data,
AADL_PORT_ACC: LNT_Channel_Data,
AADL_PORT_ACC_I: LNT_Channel_Data,
AADL_PORT_POS_I: LNT_Channel_Data]
is
loop
select
select
ACTIVATION (T_Begin);
AADL_PORT_POSITION (AADLDATA);
AADL_PORT_ACC (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ACC_I (AADLDATA);
AADL_PORT_POS_I (AADLDATA)
[]
ACTIVATION (T_All);
AADL_PORT_POSITION (AADLDATA);
AADL_PORT_ACC (AADLDATA);
AADL_PORT_ACC_I (AADLDATA);
AADL_PORT_POS_I (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
end process
process Device_Operator [
AADL_PORT_POS_C: LNT_Channel_Data]
is
loop
select
AADL_PORT_POS_C (AADLDATA)
[]
null
end select
end loop
end process
process Device_GPS [
AADL_PORT_POSITION: LNT_Channel_Data]
is
loop
select
AADL_PORT_POSITION (AADLDATA)
[]
null
end select
end loop
end process
process Device_IMU [
AADL_PORT_ANGLE: LNT_Channel_Data,
AADL_PORT_ACC: LNT_Channel_Data]
is
loop
select
AADL_PORT_ANGLE (AADLDATA)
[]
AADL_PORT_ACC (AADLDATA)
end select
end loop
end process
process Device_Platform [
AADL_PORT_ORDER: LNT_Channel_Data]
is
loop
select
AADL_PORT_ORDER (AADLDATA)
[]
null
end select
end loop
end process
end module
module FLIGHTCONTROLSYSTEM_Ports (FLIGHTCONTROLSYSTEM_Types) is
process Data_Port [
Input: LNT_Channel_Data,
Output: LNT_Channel_Data]
is
loop
select
Input (AADLDATA)
[]
Output (AADLDATA)
end select
end loop
end process
process Event_Port_Periodic [
Input: LNT_Channel_Data,
Output: LNT_Channel_Data](
Queue_Size: Nat)
is
var
Nb_Input : Nat
in
Nb_Input := 0;
loop
select
Input (AADLDATA);
if (Nb_Input < Queue_Size)
then
Nb_Input := Nb_Input + 1
end if
[]
if (Nb_Input > 0)
then
Output (AADLDATA);
Nb_Input := Nb_Input - 1
end if
end select
end loop
end var
end process
end module
module FLIGHTCONTROLSYSTEM_Types
with "==", "eq" , "<", "lt" , "<=", "le" , ">", "gt" , ">=", "ge" is
type LNT_Type_Data is
AADLDATA
end type
channel LNT_Channel_Data is
(LNT_Type_Data)
end channel
type LNT_Type_Time_Constraint is
range 0 .. 240 of Nat
end type
type LNT_Type_Thread is
array [0 .. 11 ]of LNT_Type_Time_Constraint
end type
type LNT_Type_Thread_Array is
array [1 .. 7 ]of LNT_Type_Thread
end type
type LNT_Type_Dispatch is
T_Begin, T_End, T_All, T_Preempt, T_Stop, T_Error, T_Ok
end type
type LNT_Type_Event is
Incoming_Event, No_Event
end type
channel LNT_Channel_Dispatch is
(LNT_Type_Dispatch)
end channel
channel LNT_Channel_Event is
(LNT_Type_Event)
end channel
function Thread_Number : Nat
is
return 7
end function
function PPCM_THREAD : LNT_Type_Time_Constraint
is
return LNT_Type_Time_Constraint ( 120)
end function
function _+_ (
n1: LNT_Type_Time_Constraint,
n2: LNT_Type_Time_Constraint) : LNT_Type_Time_Constraint
is
return LNT_Type_Time_Constraint (Nat (n1) + Nat (n2) mod 240)
end function
function _-_ (
n1: LNT_Type_Time_Constraint,
n2: LNT_Type_Time_Constraint) : LNT_Type_Time_Constraint
is
if (n1 < n2)
then
return LNT_Type_Time_Constraint (((240 - Nat (n2)) + Nat (n1)) mod 240)
else
return LNT_Type_Time_Constraint (Nat (n1) - Nat (n2) mod 240)
end if
end function
function _*_ (
n1: LNT_Type_Time_Constraint,
n2: LNT_Type_Time_Constraint) : LNT_Type_Time_Constraint
is
return LNT_Type_Time_Constraint (Nat (n1) * Nat (n2) mod 240)
end function
end module
module FLIGHTCONTROLSYSTEM_Processor (FLIGHTCONTROLSYSTEM_Types) is
function Assign (
in var Threads: LNT_Type_Thread_Array,
I: Nat,
K: Nat,
Val: LNT_Type_Time_Constraint) : LNT_Type_Thread_Array
is
var
P : LNT_Type_Thread
in
P := Threads[I];
P[K] := Val;
Threads[I] := P
end var;
return Threads
end function
function Update_Thread (
in var Aux_Threads: LNT_Type_Thread_Array,
I: Nat,
TODO: LNT_Type_Time_Constraint) : LNT_Type_Thread_Array
is
var
P : LNT_Type_Thread
in
P := Aux_Threads[I];
if (P[2] == LNT_Type_Time_Constraint (0))
then
P[6] := LNT_Type_Time_Constraint (1)
end if;
P[2] := P[2] + TODO;
P[8] := LNT_Type_Time_Constraint (1);
if ((P[11] == LNT_Type_Time_Constraint (1)) and (P[2] == P[0]) )
then
P[7] := LNT_Type_Time_Constraint (1);
P[2] := LNT_Type_Time_Constraint (0);
P[4] := P[5];
P[5] := PPCM_THREAD;
P[10] := LNT_Type_Time_Constraint (0)
elsif ((P[11] == LNT_Type_Time_Constraint (0)) and (P[2] == P[0]) )
then
P[7] := LNT_Type_Time_Constraint (1);
P[2] := LNT_Type_Time_Constraint (0);
P[3] := P[3] + LNT_Type_Time_Constraint (1);
P[4] := P[4] + P[1];
P[5] := P[3] * P[1]
end if;
Aux_Threads[I] := P
end var;
return Aux_Threads
end function
process Sporadic_Notif [
INCOMING_EVENT_GATE: LNT_Channel_Event](
in out Threads: LNT_Type_Thread_Array,
k: Nat,
Counter: LNT_Type_Time_Constraint,
in out Is_Activated: bool)
is
select
INCOMING_EVENT_GATE (Incoming_Event);
Threads := Assign (Threads, K, 3, (Threads[k][3] + LNT_Type_Time_Constraint (1)) )
[]
INCOMING_EVENT_GATE (No_Event)
end select ;
if ((Counter >= Threads[k][4]) and (Threads[k][3] > LNT_Type_Time_Constraint (0)) )
then
Threads := Assign (Threads, k, 4, Counter);
Threads := Assign (Threads, k, 5, (Counter + Threads[k][1]) );
Threads := Assign (Threads, k, 10, LNT_Type_Time_Constraint (1));
Threads := Assign (Threads, K, 3, (Threads[k][3] - LNT_Type_Time_Constraint (1)) );
Is_Activated := true
end if
end process