Page 209 - 《软件学报》2021年第6期

陈小颖 等:面向 CPS 时空性质验证的混成 AADL 建模与模型转换方法 1783

其中,process 为物理设备的进程;var 为物理设备的变量;interface 为物理设备的接口;time 为执行该物理设备之
间的信息交换过程的期望时间;position:=(x,y,z),x~c|y~c|z~c,c 是一个实数,~∈{>,≥,<,≤,=}.
1.4 HAADL实例
带警报的水箱控制系统,其控制器是通过传感器感知水位.当水位处于最低值 bottom 时,若 t 时间内进水系
统未响应时将会启动报警装置.当水位处于最高值 top 时,若在 t′时间内进水系统未响应时,将响应系统报警.水
位随着时间变化,水位值 y 逐渐递增 k 或递减 k.
如图 2 为带警报的水箱控制系统 AADL 模型,该进程构件包含一个线程子构件,行为附件为其中线程子构
件的计算部分的处理.对 AADL 行为附件的扩展,主要是线程中计算过程的扩展.传感器传过来的数据
sensor_data 通过连接端口传输输入给行为附件中的位置变量 y,通过行为附件的计算后,将命令数 据
command_data 通过端口传给相应的响应系统进行响应.

Fig.2 Graphical AADL model of water tank control system with alarm
图 2 带警报的水箱控制系统的图形化 AADL 模型
其中的 HAADL 行为附件描述为:
thread implementation example.impl
annex behavior_specification{**
variables
top:Base_Types::Integer;
bottom:Base_Types::Integer;
times
t:Base_Types::float;
t′:Base_Types::float;
wait:Base_Types::float;
position
y:Base_Types::Integer;
states
open:initial state;
close:complete state;
alarm:complete state;
transitions
T_0:
close[〈y=bottom〉〈(wait≤t)〉]→{open[{y=y+k}],alarm]}
T_1:
open[〈y=top〉〈(wait≤t′)〉]→{close[{y=y−k}],alarm]}
**};
end example.impl;