Page 22 - 《软件学报》2025年第4期

1428 软件学报 2025 年第 36 卷第 4 期

ICUSensorWorkingCurrentOpen!ICUDataLoadCommand?
It>=5 I_time=0 ComOn I_time<=3 ICUWork DataLoad ICUDataLib?
It<=5
It<=5 ICUSensorWorkingCurrentClose! It=0
ICUOpenPulse?
AutoOn I_time=0 It>=5 I_time>=3 It=0 ICU_Load=0
It=0 I_time>=3 2
ICUSensorWorkingCurrentOpen! AutoOff ICUClosePulse?
It=0
I_time=0 It>=5 It<=5
ICUOff 8 ComOff ICUDataLoadResult! ICU_Load=1
I_time<=3 It>=5 I_time=0 ICUSensorWorkingCurrentClose! It<=5
(f) 设备TA: IntegrateControlUnit
ICUTemperate? JPUTemperate? ICUWorkingCurrentOpenCommandFromOTPSend=1 SPUWorkingCurrentOpenCommandFromOTPSend=1
ICUOpenPulse!
ICUAutoOn SPUAutoOn
CRUTemperateRead? ICUt<=75 JPUT end1 SPUt<=75 end2
CRUT ICUt<120 ICUt>75 SPUt<120 SPUt>75
CRUTemperate? SPUTemperate?
SPUT L1 L2
JPUTemperateRead?
ICUt>=120 ICUAutoOff SPUt>=120 SPUAutoOff
TR_time<=5
ICUClosePulse!
SPUWorkingCurrentCloseCommandFromOTPSend=1
TemperateDataToDCD! ICUWorkingCurrentCloseCommandFromOTPSend=1
TR_time=0 JPUWorkingCurrentOpenCommandFromOTPSend=1 CRUAutoOff
CRUt>=120 CRUt<120
SPUTemperateRead? JPUAutoOn
CRUWorkingCurrentCloseCommandFromOTPSend=1
OTP JPUt<=75
ICUT L3
TR_time>=5 JPUt>75 JPUt<120 CRUt>75
TemperateDataSend!
end4 end3
ICUTemperateRead? JPUAutoOff JPUt>=120 CRUAutoOn CRUt<=75
JPUWorkingCurrentCloseCommandFromOTPSend=1 CRUWorkingCurrentOpenCommandFromOTPSend=1
(g) 软件构件TA: (h) 软什构件TA: OverTempProtect

TemperatureReport
图 13 验证子系统超温保护 NTA (续)

接下来对超温保护可执行验证子系统模型进行模型声明、变量和信道声明以及变量初始化. 使用 system 关
键字进行模型声明, 使用 chan 关键字声明信道, 使用 int 对整型变量进行声明. 最终包含 7 个模型声明, 26 个信道
声明, 5 个时钟变量, 8 个整型变量. 具体声明情况如表 4 所示.

表 4 验证子系统超温保护可执行验证系统声明情况

声明 声明变量
模型声明 system OverTempProtect, TemperatureReport, JPUSensor, CRUSensor, ICUSensor, SPUSensor, DisplayControlDevice
chan JPUTemperate, JPUSensorWorkingCurrentOpen, JPUSensorWorkingCurrentClose, CRUTemperate,
CRUSensorWorkingCurrentOpen, CRUSensorWorkingCurrentClose, ICUTemperate, ICUSensorWorkingCurrentOpen,
ICUSensorWorkingCurrentClose, SPUTemperate, SPUSensorWorkingCurrentOpen, SPUSensorWorkingCurrentClose,
ICUTemperateRead, ICUWorkingCurrentOpenCommandFromOTPSend, TemperateDataToDCD,
信道声明 ICUWorkingCurrentCloseCommandFromOTPSend, CRUTemperateRead, TemperateDataSend,
CRUUWorkingCurrentOpenCommandFromOTPSend, CRUWorkingCurrentCloseCommandFromOTPSend,
SPUTemperateRead, SPUWorkingCurrentOpenCommandFromOTPSend, JPUTemperateRead,
SPUWorkingCurrentCloseCommandFromOTPSend, JPUWorkingCurrentOpenCommandFromOTPSend,
JPUWorkingCurrentCloseCommandFromOTPSend
clock TR_time, ICU_workt, CRU_workt, SPU_workt, JPU_workt;
变量声明
int ICUt, CRUt, SPUt, JPUt, ICUcount, CRUcount, SPUcount, JPUcount

步骤 4: 一致性验证与不一致定位. 对于生成的一组可执行验证系统模型, 使用 UPPAAL 工具进行一致性验
证. 使用 TCTL 撰写一致性验证性质. 针对嵌入式系统中可能存在的设备调度冲突, 使用的性质模板为“A[] not 模
型 a. 状态 m and 模型 b. 状态 n”对每个设备生成相应的性质描述, 放入 UPPAAL 工具进行验证. 本案例有该类待
验证性质 10 条.
这里以超温保护可执行验证子系统模型为例, 说明一致性验证过程. 验证系统是否存在设备调度冲突, 其中涉
及一条一致性性质“A[] not OverTempProtect.ICUAutoOff and not IntegrateControlUnit.AutoOn”, 该性质验证是否存
在超温保护在温度过高时关闭 ICU 和 ICU 定时自动开关之间是否存在调度冲突, 验证结果为“不满足”. 通过不一
致性定位, 由于其他依赖需求没有问题, 则推出 OverTempProtect 存在不一致问题. 其他可执行验证子系统模型的
验证结果综合如后文表 5 所示.

5.2 方法评估
方法评估的目的就是要回答如下两个问题: 1) 本方法是否能够减少复杂嵌入式系统需求的验证状态空间?