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
A
AADLib
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
TASTE
AADLib
Commits
48d49620
Commit
48d49620
authored
Nov 26, 2018
by
yoogx
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
* Follow-up on the buses -> buses::misc renaming
For openaadl/ocarina#178
parent
3853bd3f
Changes
27
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
27 changed files
with
809 additions
and
827 deletions
+809
-827
examples/arinc653_annex/example_2/arincexample2.aadl
examples/arinc653_annex/example_2/arincexample2.aadl
+5
-5
examples/flow_analysis/flowlatencydata.aadl
examples/flow_analysis/flowlatencydata.aadl
+364
-364
examples/flow_analysis/flowlatencysampleddata.aadl
examples/flow_analysis/flowlatencysampleddata.aadl
+43
-43
examples/rap/rap.aadl
examples/rap/rap.aadl
+2
-2
examples/uxv/emaxxv2/emaxxv2_power_distrib.aadl
examples/uxv/emaxxv2/emaxxv2_power_distrib.aadl
+22
-22
examples/uxv/emaxxv2/emaxxv2_system.aadl
examples/uxv/emaxxv2/emaxxv2_system.aadl
+44
-44
examples/uxv/quadrirotorv0/quadrirotorv0_system.aadl
examples/uxv/quadrirotorv0/quadrirotorv0_system.aadl
+38
-38
examples/uxv/quadrirotorv1/quadrirotorv1_system.aadl
examples/uxv/quadrirotorv1/quadrirotorv1_system.aadl
+31
-31
examples/uxv/traxsterv3/traxsterv3_system.aadl
examples/uxv/traxsterv3/traxsterv3_system.aadl
+30
-30
src/aadl/devices/devices-battery_14v_4ah.aadl
src/aadl/devices/devices-battery_14v_4ah.aadl
+5
-6
src/aadl/devices/devices-battery_7v2_4a5h.aadl
src/aadl/devices/devices-battery_7v2_4a5h.aadl
+5
-6
src/aadl/devices/devices-camera_nc353l.aadl
src/aadl/devices/devices-camera_nc353l.aadl
+13
-14
src/aadl/devices/devices-camera_usb.aadl
src/aadl/devices/devices-camera_usb.aadl
+18
-19
src/aadl/devices/devices-inertial_gps_ig500n.aadl
src/aadl/devices/devices-inertial_gps_ig500n.aadl
+21
-22
src/aadl/devices/devices-motor_bl2824.aadl
src/aadl/devices/devices-motor_bl2824.aadl
+8
-9
src/aadl/devices/devices-motor_tm550.aadl
src/aadl/devices/devices-motor_tm550.aadl
+11
-12
src/aadl/devices/devices-odometer_refx.aadl
src/aadl/devices/devices-odometer_refx.aadl
+17
-18
src/aadl/devices/devices-receiver_smc16.aadl
src/aadl/devices/devices-receiver_smc16.aadl
+23
-24
src/aadl/devices/devices-regulator_reg113_33.aadl
src/aadl/devices/devices-regulator_reg113_33.aadl
+6
-7
src/aadl/devices/devices-regulator_ten40_4812.aadl
src/aadl/devices/devices-regulator_ten40_4812.aadl
+7
-8
src/aadl/devices/devices-regulator_tsi10n.aadl
src/aadl/devices/devices-regulator_tsi10n.aadl
+7
-8
src/aadl/devices/devices-router_wifi_wndr3300.aadl
src/aadl/devices/devices-router_wifi_wndr3300.aadl
+13
-14
src/aadl/devices/devices-telemeter_urg04lx.aadl
src/aadl/devices/devices-telemeter_urg04lx.aadl
+14
-15
src/aadl/devices/devices-telemeter_utm30lx.aadl
src/aadl/devices/devices-telemeter_utm30lx.aadl
+13
-14
src/aadl/devices/devices-ultrasound_sfr08.aadl
src/aadl/devices/devices-ultrasound_sfr08.aadl
+15
-16
src/aadl/devices/devices-variator_blctlv12.aadl
src/aadl/devices/devices-variator_blctlv12.aadl
+15
-16
src/aadl/devices/devices-variator_evx.aadl
src/aadl/devices/devices-variator_evx.aadl
+19
-20
No files found.
examples/arinc653_annex/example_2/arincexample2.aadl
View file @
48d49620
...
...
@@ -37,7 +37,7 @@ package arincexample2
public
with
ARINC653
;
with
buses
;
with
buses
::
misc
;
with
memories
;
with
processors
;
--
First
,
define
generic
component
...
...
@@ -47,8 +47,8 @@ public
memory
memchunk
extends
memories
::
ROM
end
memchunk
;
memory
mainmemory
extends
memories
::
ROM
end
mainmemory
;
bus
anybus
extends
buses
::
generic_bus
end
anybus
;
bus
implementation
anybus
.
i
extends
buses
::
generic_bus
.
impl
end
anybus
.
i
;
bus
anybus
extends
buses
::
misc
::
generic_bus
end
anybus
;
bus
implementation
anybus
.
i
extends
buses
::
misc
::
generic_bus
.
impl
end
anybus
.
i
;
thread
network_driver_thread
properties
...
...
@@ -64,13 +64,13 @@ public
--
JH
addition
abstract
network_driver_partition_holder
end
network_driver_partition_holder
;
abstract
implementation
network_driver_partition_holder
.
i
subcomponents
ndp
:
process
network_driver_partition
.
i
;
end
network_driver_partition_holder
.
i
;
--
/
JH
addition
process
network_driver_partition
end
network_driver_partition
;
...
...
examples/flow_analysis/flowlatencydata.aadl
View file @
48d49620
This diff is collapsed.
Click to expand it.
examples/flow_analysis/flowlatencysampleddata.aadl
View file @
48d49620
...
...
@@ -35,7 +35,7 @@
--
--
The
sampling
latency
is
affected
by
whether
the
system
operates
--
with
respect
to
a
global
clock
(
synchronous
system
)
or
independent
--
clock
(
asynchronous
system
).
--
clock
(
asynchronous
system
).
--
--
The
models
below
are
set
up
to
execute
under
a
synchronous
and
an
--
asynchronous
system
.
...
...
@@ -43,8 +43,8 @@
package
Flowlatencysampleddata
public
with
processors
;
with
buses
;
with
buses
::
misc
;
data
timedata
end
timedata
;
...
...
@@ -61,7 +61,7 @@ public
--
--
Step1
executes
at
a
rate
of
20
Hz
and
has
a
deadline
or
maximum
--
latency
of
45
ms
.
thread
step1
features
ined
:
in
event
data
port
timedata
{
Queue_Size
=>
0
;
};
...
...
@@ -78,12 +78,12 @@ public
properties
Dispatch_Protocol
=>
Periodic
;
end
step1
.
periodic
;
thread
implementation
step1
.
aperiodic
properties
Dispatch_Protocol
=>
Aperiodic
;
end
step1
.
aperiodic
;
--
step2
??
thread
step2
...
...
@@ -97,17 +97,17 @@ public
deadline
=>
70
ms
;
Compute_Execution_Time
=>
15
ms
..
23
ms
;
end
step2
;
thread
implementation
step2
.
periodic
properties
Dispatch_Protocol
=>
Periodic
;
end
step2
.
periodic
;
thread
implementation
step2
.
aperiodic
properties
Dispatch_Protocol
=>
Aperiodic
;
end
step2
.
aperiodic
;
--
step3
??
thread
step3
...
...
@@ -121,20 +121,20 @@ public
deadline
=>
45
ms
;
Compute_Execution_Time
=>
6
ms
..
10
ms
;
end
step3
;
thread
implementation
step3
.
periodic
properties
Dispatch_Protocol
=>
Periodic
;
end
step3
.
periodic
;
thread
implementation
step3
.
aperiodic
properties
Dispatch_Protocol
=>
Aperiodic
;
end
step3
.
aperiodic
;
--
At
the
beginning
of
each
dispatch
the
sensor
device
reads
the
--
clock
and
passes
it
as
the
value
of
its
output
device
sensor
features
outed
:
out
event
data
port
timedata
;
...
...
@@ -146,13 +146,13 @@ public
deadline
=>
2
ms
;
Compute_Execution_Time
=>
1
ms
..
2
ms
;
end
sensor
;
--
sensor
periodically
senses
the
physical
environment
device
implementation
sensor
.
periodic
properties
Dispatch_Protocol
=>
Periodic
;
end
sensor
.
periodic
;
--
Then
sensor
detects
an
in
the
physical
environment
occurs
--
randomly
with
a
maximum
rate
of
the
period
...
...
@@ -160,10 +160,10 @@ public
properties
Dispatch_Protocol
=>
Aperiodic
;
end
sensor
.
aperiodic
;
--
The
actuator
will
read
the
clock
and
log
the
difference
to
the
--
received
data
(
sensor
clock
time
)
as
its
last
action
device
actuator
features
ined
:
in
event
data
port
timedata
{
Queue_Size
=>
0
;
};
...
...
@@ -175,7 +175,7 @@ public
deadline
=>
3
ms
;
Compute_Execution_Time
=>
1
ms
..
3
ms
;
end
actuator
;
--
output
is
sampled
.
This
reduces
the
latency
jitter
device
implementation
actuator
.
periodic
...
...
@@ -183,13 +183,13 @@ public
Dispatch_Protocol
=>
Periodic
;
end
actuator
.
periodic
;
--
arrival
of
data
causes
actuator
to
become
active
.
--
arrival
of
data
causes
actuator
to
become
active
.
--
This
reduces
end
-
to
-
end
latency
at
the
expense
of
increased
jitter
.
device
implementation
actuator
.
aperiodic
properties
Dispatch_Protocol
=>
Aperiodic
;
end
actuator
.
aperiodic
;
process
Pstep1
features
ined
:
in
event
data
port
timedata
;
...
...
@@ -197,7 +197,7 @@ public
flows
flow1
:
flow
path
ined
->
outed
;
end
Pstep1
;
process
implementation
Pstep1
.
periodic
subcomponents
Tstep1
:
thread
Step1
.
periodic
;
...
...
@@ -207,7 +207,7 @@ public
flows
flow1
:
flow
path
ined
->
cin
->
Tstep1
.
flow1
->
cout
->
outed
;
end
Pstep1
.
periodic
;
process
implementation
Pstep1
.
aperiodic
subcomponents
Tstep1
:
thread
Step1
.
aperiodic
;
...
...
@@ -225,7 +225,7 @@ public
flows
flow1
:
flow
path
ined
->
outed
;
end
Pstep2
;
process
implementation
Pstep2
.
periodic
subcomponents
Tstep2
:
thread
Step2
.
periodic
;
...
...
@@ -235,7 +235,7 @@ public
flows
flow1
:
flow
path
ined
->
cin
->
Tstep2
.
flow1
->
cout
->
outed
;
end
Pstep2
.
periodic
;
process
implementation
Pstep2
.
aperiodic
subcomponents
Tstep2
:
thread
Step2
.
aperiodic
;
...
...
@@ -253,7 +253,7 @@ public
flows
flow1
:
flow
path
ined
->
outed
;
end
Pstep3
;
process
implementation
Pstep3
.
periodic
subcomponents
Tstep3
:
thread
Step3
.
periodic
;
...
...
@@ -263,7 +263,7 @@ public
flows
flow1
:
flow
path
ined
->
cin
->
Tstep3
.
flow1
->
cout
->
outed
;
end
Pstep3
.
periodic
;
process
implementation
Pstep3
.
aperiodic
subcomponents
Tstep3
:
thread
Step3
.
aperiodic
;
...
...
@@ -278,7 +278,7 @@ public
features
db
:
requires
bus
access
devicebus
.
basic
;
end
application
;
--
This
application
configuration
has
all
processing
steps
as
well
--
as
the
sensor
and
actuator
as
periodic
tasks
.
--
...
...
@@ -347,32 +347,32 @@ public
->
compute12
->
compute2
.
flow1
->
compute23
->
compute3
.
flow1
->
actuateconn
->
actuate
.
flow1
{
latency
=>
165
ms
..
165
ms
;};
end
application
.
alldatadriven
;
--
hardware
platforms
:
single
processor
,
dual
processor
processor
singleCPU
extends
processors
::
generic_cpu
features
db
:
requires
bus
access
devicebus
.
basic
;
pb
:
requires
bus
access
cpubus
;
end
singleCPU
;
processor
implementation
singleCPU
.
basic
end
singleCPU
.
basic
;
bus
cpubus
extends
buses
::
generic_bus
end
cpubus
;
bus
implementation
cpubus
.
basic
extends
buses
::
generic_bus
.
impl
end
cpubus
.
basic
;
bus
devicebus
extends
buses
::
generic_bus
end
device
bus
;
bus
cpubus
extends
buses
::
misc
::
generic_bus
end
cpu
bus
;
bus
implementation
devicebus
.
basic
extends
buses
::
generic_bus
.
impl
bus
implementation
cpubus
.
basic
extends
buses
::
misc
::
generic_bus
.
impl
end
cpubus
.
basic
;
bus
devicebus
extends
buses
::
misc
::
generic_bus
end
devicebus
;
bus
implementation
devicebus
.
basic
extends
buses
::
misc
::
generic_bus
.
impl
end
devicebus
.
basic
;
system
hardwareplatform
features
db
:
provides
bus
access
devicebus
.
basic
;
end
hardwareplatform
;
system
implementation
hardwareplatform
.
single
subcomponents
cpu1
:
processor
singleCPU
.
basic
;
...
...
@@ -381,7 +381,7 @@ public
W5
:
bus
access
db1
->
cpu1
.
db
;
W6
:
bus
access
db1
->
db
;
end
hardwareplatform
.
single
;
system
implementation
hardwareplatform
.
dual
subcomponents
cpu1
:
processor
singleCPU
.
basic
;
...
...
@@ -395,11 +395,11 @@ public
end
hardwareplatform
.
dual
;
--
system
configurations
:
hardware
and
application
system
topsystem
end
topsystem
;
--
first
all
single
processor
configurations
system
implementation
topsystem
.
allperiodicsampled
subcomponents
app
:
system
application
.
allperiodicsampled
;
...
...
@@ -409,7 +409,7 @@ public
properties
Actual_Processor_Binding
=>
(
reference
(
hw
.
cpu1
))
applies
to
app
;
end
topsystem
.
allperiodicsampled
;
system
implementation
topsystem
.
alldatadriven
subcomponents
app
:
system
application
.
alldatadriven
;
...
...
@@ -419,13 +419,13 @@ public
properties
Actual_Processor_Binding
=>
(
reference
(
hw
.
cpu1
))
applies
to
app
;
end
topsystem
.
alldatadriven
;
--
The
same
application
sytems
can
be
configured
with
a
two
--
processor
system
.
We
are
showing
one
configuration
where
the
--
second
step
is
located
on
a
second
processor
.
In
this
case
the
--
end
-
to
-
end
latency
is
increased
by
any
communication
latency
--
between
the
two
processors
across
the
bus
system
implementation
topsystem
.
distributedalldatadriven
subcomponents
app
:
system
application
.
alldatadriven
;
...
...
examples/rap/rap.aadl
View file @
48d49620
...
...
@@ -4,7 +4,7 @@ public
with
Deployment
;
with
Transformations
;
with
processors
;
with
buses
;
with
buses
::
misc
;
with
memories
;
----------
...
...
@@ -2006,7 +2006,7 @@ end cpu.impl;
--
Bus
--
---------
bus
C_Bus
extends
buses
::
generic_bus
bus
C_Bus
extends
buses
::
misc
::
generic_bus
end
C_Bus
;
bus
implementation
C_Bus
.
Impl
...
...
examples/uxv/emaxxv2/emaxxv2_power_distrib.aadl
View file @
48d49620
...
...
@@ -4,7 +4,7 @@ public
--
with
AT91SAM7A3
;
--
with
AT91SAM9G20
;
with
buses
;
with
buses
::
misc
;
with
devices
::
ultrasound_sfr08
;
with
devices
::
odometer_refx
;
...
...
@@ -32,54 +32,54 @@ public
system
implementation
emaxxv2
.
power
subcomponents
---------------------
POWER
NETS
----------------
VBat_bus
:
bus
buses
::
VBat_bus
.
impl
;
V5_1_bus
:
bus
buses
::
V5_bus
.
impl
;
V5_2_bus
:
bus
buses
::
V5_bus
.
impl
;
--
V3v3_bus
:
bus
buses
::
V3v3_bus
.
impl
;
V12_bus
:
bus
buses
::
V12_bus
.
impl
;
VBatmotors_bus
:
bus
buses
::
VBat_bus
.
impl
;
VBat_bus
:
bus
buses
::
misc
::
VBat_bus
.
impl
;
V5_1_bus
:
bus
buses
::
misc
::
V5_bus
.
impl
;
V5_2_bus
:
bus
buses
::
misc
::
V5_bus
.
impl
;
--
V3v3_bus
:
bus
buses
::
misc
::
V3v3_bus
.
impl
;
V12_bus
:
bus
buses
::
misc
::
V12_bus
.
impl
;
VBatmotors_bus
:
bus
buses
::
misc
::
VBat_bus
.
impl
;
---------------------
ARM7
----------------------
US1
:
device
devices
::
ultrasound_sfr08
::
US
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
US2
:
device
devices
::
ultrasound_sfr08
::
US
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
ODOMETER1
:
device
devices
::
odometer_refx
::
ODOMETER
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
ODOMETER2
:
device
devices
::
odometer_refx
::
ODOMETER
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
RECEIVER
:
device
devices
::
receiver_smc16
::
RECEIVER
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
--
CPU_ARM7
:
processor
AT91SAM7A3
::
ARM7
.
impl
--
{
Electricity_Properties
::
Power_Level
=>
3
;};
----------------------
ARM9
----------------------
INERTIAL_GPS
:
device
devices
::
inertial_gps_ig500n
::
INERTIAL_GPS
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
TELEMETER
:
device
devices
::
telemeter_utm30lx
::
TELEMETER
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
CAMERA_IP
:
device
devices
::
camera_nc353l
::
CAMERA_IP
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
ROUTER_WIFI
:
device
devices
::
router_wifi_wndr3300
::
ROUTER_WIFI
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
VARIATOR
:
device
devices
::
variator_evx
::
VARIATOR
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
MOTORS
:
device
devices
::
motor_tm550
::
MOTOR_TM550
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
--
CPU_ARM9
:
processor
AT91SAM9G20
::
ARM9
.
impl
--
{
Electricity_Properties
::
Power_Level
=>
2
;};
---------------------
REGULATORS
-----------------
REG_5V_1
:
device
devices
::
regulator_TSI10N
::
REG_5V
.
impl
--
reg
embedded
into
ARM7
board
{
Electricity_Properties
::
Power_Level
=>
1
;};
REG_5V_2
:
device
devices
::
regulator_TSI10N
::
REG_5V
.
impl
{
Electricity_Properties
::
Power_Level
=>
1
;};
{
Electricity_Properties
::
Power_Level
=>
1
;};
REG_12V
:
device
devices
::
regulator_ten40_4812
::
REG_12V
.
impl
{
Electricity_Properties
::
Power_Level
=>
1
;};
{
Electricity_Properties
::
Power_Level
=>
1
;};
REG_3V3
:
device
devices
::
regulator_reg113_33
::
REG_3V3
.
impl
{
Electricity_Properties
::
Power_Level
=>
2
;};
{
Electricity_Properties
::
Power_Level
=>
2
;};
---------------------
BATERIES
-----------------
BAT_14V_CALC
:
device
devices
::
battery_14v_4ah
::
BAT_14V_4AH
.
impl
{
Electricity_Properties
::
Power_Level
=>
0
;};
{
Electricity_Properties
::
Power_Level
=>
0
;};
BAT_14V_MOTORS
:
device
devices
::
battery_14v_4ah
::
BAT_14V_4AH
.
impl
{
Electricity_Properties
::
Power_Level
=>
0
;};
{
Electricity_Properties
::
Power_Level
=>
0
;};
connections
------------------------------------------------------------------
...
...
examples/uxv/emaxxv2/emaxxv2_system.aadl
View file @
48d49620
package
emaxxv2_system
public
public
with
Deployment
;
With
Electricity_Properties
;
with
buses
;
with
buses
::
misc
;
with
Buses
::
I2C
;
with
Buses
::
USB
;
with
Buses
::
UART
;
with
Buses
::
UART
;
with
Buses
::
Ethernet
;
with
Processors
::
ARM
;
with
devices
::
ultrasound_sfr08
;
with
devices
::
odometer_refx
;
with
devices
::
receiver_smc16
;
with
devices
::
inertial_gps_ig500n
;
with
devices
::
telemeter_utm30lx
;
with
devices
::
camera_nc353l
;
with
devices
::
router_wifi_wndr3300
;
with
emaxxv2_sw
;
------------
--
System
--
------------
system
emaxxv2
system
emaxxv2
end
emaxxv2
;
system
implementation
emaxxv2
.
impl
subcomponents
------------------------------------------------------------------
--
IPC
bus
between
CICAS
&
CCDS
------------------------------------------------------------------
UART_IPC_bus
:
bus
buses
::
UART
::
UART
.
impl
;
------------------------------------------------------------------
--
Node
#
1
hardware
components
:
CICAS
(
ARM7
card
)
------------------------------------------------------------------
...
...
@@ -41,7 +41,7 @@ public
--
sensors
/
actautors
to
support
communication
through
various
protocols
------------------------------------------------------------------
I2C_bus
:
bus
Buses
::
I2C
::
I2C
.
impl
;
TIMER_bus_ARM7
:
bus
buses
::
TIMER_bus
.
impl
;
TIMER_bus_ARM7
:
bus
buses
::
misc
::
TIMER_bus
.
impl
;
------------------------------------------------------------------
--
Hardware
components
for
CICAS
configuration
------------------------------------------------------------------
...
...
@@ -52,21 +52,21 @@ public
------------------------------------------------------------------
US1
:
device
devices
::
ultrasound_sfr08
::
US
.
impl
{
Deployment
::
Location
=>
"0xE0"
;};
--
define
here
the
address
of
US1
TWI_ARM7
:
device
Processors
::
ARM
::
TWI_Peripheral
.
impl
;
UART0_ARM7
:
device
Processors
::
ARM
::
USART0_Peripheral
.
impl
;
TWI_ARM7
:
device
Processors
::
ARM
::
TWI_Peripheral
.
impl
;
UART0_ARM7
:
device
Processors
::
ARM
::
USART0_Peripheral
.
impl
;
TIMER_ARM7
:
device
Processors
::
ARM
::
TIMER_Peripheral
.
impl
;
PWM_ARM7
:
device
Processors
::
ARM
::
PWM_Peripheral
.
impl
;
PWM_ARM7
:
device
Processors
::
ARM
::
PWM_Peripheral
.
impl
;
------------------------------------------------------------------
--
End
Node
#
1
------------------------------------------------------------------
------------------------------------------------------------------
--
Node
#
2
hardware
components
:
CCDS
(
ARM9
card
)
------------------------------------------------------------------
--
CCDS
Interconnect
bus
.
This
component
are
shared
by
ARM9
--
peripherals
and
sensors
/
actautors
to
support
communication
--
through
various
protocols
------------------------------------------------------------------
USB1_bus
:
bus
buses
::
USB
::
USB
.
impl
;
UART2_bus
:
bus
buses
::
UART
::
UART
.
impl
;
...
...
@@ -81,41 +81,41 @@ public
--
Processor
peripherals
for
CCDS
communication
with
sensors
------------------------------------------------------------------
UART0_ARM9
:
device
Processors
::
ARM
::
USART0_Peripheral
.
impl
{
Electricity_Properties
::
Device_Type
=>
Master
;};
--
Refined
Property
(
UART0_ARM9
and
UART0_ARM7
devices
inherit
--
the
same
device
)
for
checking
Electrical_Compatibility
theorem
UART2_ARM9
:
device
Processors
::
ARM
::
USART2_Peripheral
.
impl
;
USB1_ARM9
:
device
Processors
::
ARM
::
USB1_Peripheral
.
impl
;
ETHERNET_ARM9
:
device
Processors
::
ARM
::
ETHERNET_Peripheral
.
impl
;
{
Electricity_Properties
::
Device_Type
=>
Master
;};
--
Refined
Property
(
UART0_ARM9
and
UART0_ARM7
devices
inherit
--
the
same
device
)
for
checking
Electrical_Compatibility
theorem
UART2_ARM9
:
device
Processors
::
ARM
::
USART2_Peripheral
.
impl
;
USB1_ARM9
:
device
Processors
::
ARM
::
USB1_Peripheral
.
impl
;
ETHERNET_ARM9
:
device
Processors
::
ARM
::
ETHERNET_Peripheral
.
impl
;
------------------------------------------------------------------
--
End
Node
#
2
------------------------------------------------------------------
------------------------------------------------------------------
--
List
of
sensors
/
actuators
------------------------------------------------------------------
---------------------
ARM7
----------------------
US2
:
device
devices
::
ultrasound_sfr08
::
US
.
impl
{
Deployment
::
Location
=>
"0xE4"
;};
--
define
here
the
address
of
US2
ODOMETER1
:
device
devices
::
odometer_refx
::
ODOMETER
.
impl
;
ODOMETER2
:
device
devices
::
odometer_refx
::
ODOMETER
.
impl
;
RECEIVER
:
device
devices
::
receiver_smc16
::
RECEIVER
.
impl
;
----------------------
ARM9
----------------------
INERTIAL_GPS
:
device
devices
::
inertial_gps_ig500n
::
INERTIAL_GPS
.
impl
;
TELEMETER
:
device
devices
::
telemeter_utm30lx
::
TELEMETER
.
impl
;
CAMERA_IP
:
device
devices
::
camera_nc353l
::
CAMERA_IP
.
impl
;
ROUTER_WIFI
:
device
devices
::
router_wifi_wndr3300
::
ROUTER_WIFI
.
impl
;
connections
------------------------------------------------------------------
--
System
bus
connections
:
between
CCDS
&
CICAS
--
System
bus
connections
:
between
CCDS
&
CICAS
--
USART
serial
line
,
it
is
shared
by
CICAS
and
CCDS
to
support
--
communication
through
the
serial
line
.
------------------------------------------------------------------
F1
:
bus
access
UART_IPC_bus
->
UART0_ARM9
.
Serial_Wire
;
F2
:
bus
access
UART_IPC_bus
->
UART0_ARM7
.
Serial_Wire
;
------------------------------------------------------------------
--
Node
#
1
bus
connections
:
CICAS
(
ARM7
card
)
------------------------------------------------------------------
...
...
@@ -127,7 +127,7 @@ public
F7
:
bus
access
TIMER_bus_ARM7
->
ODOMETER1
.
Serial_Wire
;
F8
:
bus
access
TIMER_bus_ARM7
->
ODOMETER2
.
Serial_Wire
;
F9
:
bus
access
TIMER_bus_ARM7
->
RECEIVER
.
Serial_Wire
;
--
--
------------------------------------------------------------------
--
Node
#
2
bus
connections
:
CCDS
(
ARM9
card
)
------------------------------------------------------------------
...
...
@@ -141,47 +141,47 @@ public
F15
:
bus
access
ETHERNET2_bus
->
CAMERA_IP
.
PortCom
;
F16
:
bus
access
ETHERNET1_bus
->
ROUTER_WIFI
.
Port1
;
F17
:
bus
access
ETHERNET2_bus
->
ROUTER_WIFI
.
Port2
;
EventCnx1
:
port
proc_1
.
US1_evt
->
US1
.
proc_evt
;
EventCnx2
:
port
proc_1
.
US2_evt
->
US2
.
proc_evt
;
EventCnx3
:
port
proc_1
.
Odometer1_evt
->
ODOMETER1
.
proc_evt
;
EventCnx4
:
port
proc_1
.
Odometer2_evt
->
ODOMETER2
.
proc_evt
;
EventCnx5
:
port
proc_1
.
Receiver_evt
->
RECEIVER
.
proc_evt
;
EventCnx1
:
port
proc_1
.
US1_evt
->
US1
.
proc_evt
;
EventCnx2
:
port
proc_1
.
US2_evt
->
US2
.
proc_evt
;
EventCnx3
:
port
proc_1
.
Odometer1_evt
->
ODOMETER1
.
proc_evt
;
EventCnx4
:
port
proc_1
.
Odometer2_evt
->
ODOMETER2
.
proc_evt
;
EventCnx5
:
port
proc_1
.
Receiver_evt
->
RECEIVER
.
proc_evt
;
properties
--
The
processor
CPU
runs
the
process
and
the
TWI
driver
for
I2C
connexion
Actual_Processor_Binding
=>
(
reference
(
CPU_ARM7
))
applies
to
proc_1
;
--
Actual_Processor_Binding
=>
(
reference
(
CPU_ARM9
))
applies
to
proc_2
;
annex
real_specification
{**
--
Electricity_Prop_Defined
and
Utilization_prop_def
theorems
--
are
required
for
analysis
Current_Drain
and
Electrical_Compatibility
theorems
--
Electricity_Prop_Defined
and
Utilization_prop_def
theorems
--
are
required
for
analysis
Current_Drain
and
Electrical_Compatibility
theorems
theorem
Electricity_Prop_Defined
foreach
e
in
Device_Set
do
requires
(
Electricity_Prop_Defined
);
check
(
1
=
1
);
end
Electricity_Prop_Defined
;
theorem
Utilization_prop_def
foreach
e
in
Thread_Set
do
requires
(
Utilization_prop_def
);
check
(
1
=
1
);
end
Utilization_prop_def
;