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

1790 Journal of Software 软件学报 Vol.32, No.6, June 2021

Table 1 Mapping rules from HAADL to HP-TCSP
表 1 HAADL 到 HP-TCSP 映射规则
Name Description
Integer2IntegerType Integer2IntegerType Match HAADL.IntegerType to HP-TCSP.Integer
Float2RealType Float2RealType Match HAADL.floatType to HP-TCSP.Real
Boolean2BooleanType Boolean2BooleanType Match HAADL.BooleanType to HP-TCSP.Boolean
String2StringType String2StringType Match HAADL.StringType to HP-TCSP.String
state2process state2process Match HAADL.state to HP-TCSP.process
timetrigger2overtime timetrigger2overtime Match HAADL.timetrigger to HP-TCSP. P Q d
conditiontrigger2ConFcon conditiontrigger2ConFcon Match HAADL.conditiontrigger to HP-TCSP.Con and HP-TCSP.Fcon
Inoutput2Inoutput Inoutput2Inoutput Match HAADL.input and HAADL.output to HP-TCSP.input and HP-TCSP.output
act2assignment act2assignment Match HAADL.act to HP-TCSP.assignment
assignment2assignment assignment2assignment Match HAADL.assignment to HP-TCSP.assignment
sameact2and sameact2and Match HAADL.| to HP-TCSP||
interrupt2interrupt interrupt2interrupt Match HAADL.interrupt to HP-TCSP.condition interrupt
3.4 转换实例
接下来将第 1.4 节带警报的水箱控制系统扩展的行为附件部分转换成相应的 HP-TCSP 模型.
首先,将 variables,times,position 中的 Integer 与 float 分别转换为 HP-TCSP 离散变量集合中的 InterType 与
RealType 类型.状态 open,close,alarm 转换为进程变量 OPEN,CLOSE,ALARM 以及其他条件执行与条件中断等.
具体转换见表 2.
Table 2 Mapping rules from HAADL to HP-TCSP for water tank control system
表 2 水箱控制系统 HAADL 到 HP-TCSP 映射规则
HAADL HP-TCSP HAADL HP-TCSP
Integer top Integer top open OPEN
Integer bottom Integer bottom close CLOSE
float t Real t alarm ALARM
float t′ Real t′ y=y+1 y?(y+1)
float wait Real wait y≠bottom (y≠bottom&wait<t)>>OPEN
Integer y Integer y y≠top (y≠top&wait<t′)>>CLOSE
conditioninterrupt OPEN (y=top)&&(wait>t′)AALARM conditioninterrupt CLOSE (y=bottom&&wait>t)AALARM

转换后,HP-TCSP 如下:
• 离散变量集合 DV:={top,bottom,t,t′,wait,y};
• 进程变量集合 PV:={OPEN,CLOSE,ALARM}.
其中,
WATER=OPEN (y=top)&&(wait>t′)AALARM||CLOSE (y=bottom&&wait>t)AALARM;
OPEN=y=(y+k)→STOP;
CLOSE=y=(y−k)→STOP;
ALARM=alarm→STOP.

4 实例分析

飞机避撞系统是典型的 CPS 应用实例,对飞机避撞系统的安全性研究也是研究热点之一.2000 年~2014 年
间,美国空军的 F-16 战斗机因可控飞行撞地事故而损失的飞行员人数占到了所有非发动机失效相关事故的
75%.美国空军研究实验室(AFRL)研究发现,飞机发生与地面或其他飞机相撞事故的起因包括加速度致飞行员
意识丧失(G-LOC)、空间迷向、飞行员过于盯住目标、注意力分散和任务饱和等.因此,保证飞机避撞系统的安
全性十分必要.下面我们通过一个飞机避撞系统的实例,给出 AADL 的行为附件的描述并且利用转换规则转换
为形式化的 HP-TCSP 验证其时空的一致性,从而验证避撞系统的安全性.

现研究一个竖直平面的飞机避撞系统,假设飞机处于同一竖直平面位置.如图 7 所示:假设两架飞机 p 1 与 p 2