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

杨晓 等: 复杂嵌入式系统需求一致性的组合验证方法 1429

2) 本方法能够提高验证的效率么? 我们考虑采用对比实验, 对比我们的方法对案例的组合验证效果以及整体验证
的效果, 对比两次实验来判断本方法是否能够减少验证系统的状态空间以及是否能够提高验证效率.

表 5 机载侦查子系统调度冲突一致性验证结果综合

验证子系统 验证结果
综合控制单元加电控制 (ICUPowerOpenControl) 不涉及设备, 无相关验证
综合控制单元断电控制 (ICUPowerCloseControl) 不涉及设备, 无相关验证
信号处理单元加电控制 (SPUPowerOpenControl) 不涉及设备, 无相关验证
信号处理单元断电控制 (SPUPowerCloseControl) 不涉及设备, 无相关验证
采集接收单元加电控制 (CRUPowerOpenControl) 不涉及设备, 无相关验证
采集接收单元断电控制 (CRUPowerCloseControl) 不涉及设备, 无相关验证
干扰处理单元加电控制 (JPUPowerOpenControl) 不涉及设备, 无相关验证
干扰处理单元断电控制 (JPUPowerCloseControl) 不涉及设备, 无相关验证
生成8条性质, 6条不满足, 发现设备ICU、CRU、SPU和JPU存在设备调度冲
信号电流控制 (WorkingCurrentControl)
突, WorkingCurrentControl存在不一致
生成1条性质, 不满足, 发现设备LandingGear和Transmitters存在设备调度冲
初始化 (Initialization)
突, WorkingCurrentControl存在不一致
数据加载 (DataLoad) 不涉及设备, 无相关验证
信号分选 (SignalSort) 不涉及设备, 无相关验证
频谱监测 (SpectrumSurveillance) 不涉及设备, 无相关验证
目标上报 (TargetReport) 不涉及设备, 无相关验证
信号识别 (SignalIdentify) 不涉及设备, 无相关验证
侦查引导 (ReconnaissanceGuide) 不涉及设备, 无相关验证
干扰处理 (JamProcess) 不涉及设备, 无相关验证
温度上报 (TemperatureReport) 不涉及设备, 无相关验证
生成1条性质, 不满足, 发现设备ICU存在设备调度冲突, 通过不一致性得出
超温保护 (OverTempProtect)
OverTempProtect存在不一致
误定位.

5.2.1 实验预备
在本实验中, 我们选择了 5 个不同的案例进行实验, 分别为灯光控制系统、智能家居控制子系统、机载侦查
控制系统、轨道交通车载控制子系统和航天领域太阳搜索控制子系统. 其中涉及的需求数量从 2–19 个不等, 设备
也涉及 5–28 个不等, 含有不同数量的数据依赖和控制依赖. 实验使用的软件环境为 UPPAAL-4.1.24, 使用硬件设
备环境为 Windows 10 系统, 32 GB 运行内存, 1 TB SSD.

5.2.2 实验过程
首先为上述 5 个案例中的每个案例的设备建立设备知识库, 将其中涉及的设备进行 TA 建模. 然后采用本文
组合验证方法对需求的一致性进行验证. 根据每个案例的问题图以及建立的领域设备知识库识别每个案例中的控
制依赖和数据依赖关系. 接着以每个案例中的子需求为关注点, 生成验证子系统架构, 生成可执行验证系统模型.
最后对各个案例中的验证子系统进行一致性验证, 对一致性验证结果进行综合, 并对不满足一致性的情况进行错

针对该问题的对比实验, 我们使用设备调度冲突一致性验证性质, 根据模板“A[] not 模型 a. 状态 m and 模型
b. 状态 n”进行性质生成, 我们记录其需求依赖关系、验证结果及验证子系统的状态空间和运行时间. 需要特别强
调的是, 在验证性质中涉及到的多个设备冲突检测, 使得每个验证性质都对应着不同的状态空间. 接下来, 我们采
用整体验证方法, 不考虑依赖关系, 将上述的验证子系统中的软件构件、设备构件合并在一起运行, 进行一致性验
证. 在整体验证方法中使用的一致性验证性质与组合验证方法中使用的一致性性质同为一组性质. 记录其验证结
果、验证系统的状态空间和运行时间. 其中也涉及多个验证性质的多组验证.