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

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

Out of memory Out of memory
35 000 000 35 000 000
30 000 000 30 000 000
18 025 481
25 000 000 17 282 938 25 000 000 18 025 481
状态空间 20 000 000 16 837 263 状态空间 20 000 000 17 232 118
17 282 938
17 232 118
297 508
15 000 000
252 494 15 000 000 16 837 263
10 000 000 187 608 10 000 000 297 508
155 312 155 312
5 000 000 132 468 5 000 000 132 468
117 916 117 916
0 0
组合验证 整体验证 组合验证 整体验证
状态空间 状态空间 状态空间 状态空间
(d) 机载侦查控制子系统 (e) 太阳搜索控制子系统
图 14 各案例组合验证与整体验证状态数对比结果 (续)

方法在应对复杂系统需求验证时, 能有效提升效率.
5.2.3 结果分析
从表 6 中可以看出, 我们的组合验证方法表现良好, 针对每组案例都能得到验证结果. 特别是针对规模较大的
机载侦查子系统和太阳搜索控制子系统, 原先的整体模型验证受限于 UPPAAL 工具的验证能力, 发生了超出内存
无法验证的情况, 而我们的方法可以通过组合子系统约减状态空间来进行验证, 得到验证结果, 这说明我们的方法
有着应对复杂系统的能力. 结合图 14(d) 和 (e), 可以看出这两个复杂系统在进行整体验证时探索的状态数高于
10 亿, 而通过我们的组合验证方法, 其探索的子系统的状态数最多在千万级别. 另外, 从可验证系统的角度来看,
如灯光控制系统、智能家居控制系统和轨道交通控制子系统, 本文方法已经将探索的状态空间减少了至少
25.78%. 虽然这些数据只是针对验证子系统而言, 但这两组数据充分说明本文方法能够有效地约减待验证系统的
状态空间. 对于超出内存限制的整体模型验证, 如机载侦查子系统和太阳搜索控制子系统, 本文的方法仍然能够进
行有效验证, 这显然在减少验证状态空间方面起到了有效作用. 然而, 这并不意味着各验证子系统探索状态的总和
一定少于整体验证系统的状态, 例如在图 14(b) 的智能家居系统中, 两个子验证系统探索的状态总和已经超过了
整体验证状态.
关于验证效率, 从表 6 中可以看出, 对于相对简单的案例, 如灯光控制系统和轨道交通控制子系统, 其验证状
态空间值低于 100 (图 14(a) 和图 14(c)), 在验证过程中并未花费任何时间. 因此对于这类较小的案例, 组合验证方
法与整体模型验证方法在时间消耗上并无差别. 然而, 对于稍微复杂一些的系统, 例如智能家居控制子系统 (如
图 14(b) 所示), 其状态空间可以达到 10 万级别. 通过比较各子系统验证与整体验证所需的最大时间, 我们发现时
间消耗可以降低至少 24.80%. 值得注意的是, 这个时间减少是指每个子系统与整体验证系统相比, 而并非所有子
系统验证时间的总和. 若将所有子系统的验证时间加起来, 可能会超过整体系统的验证时间. 这说明对于这类规模
还能做整体验证的系统, 本文方法可能并不实用. 对于更加复杂的系统, 如机载侦查子系统和太阳搜索子系统
(图 14(d) 和图 14(e)), 其在组合验证方法中验证空间大小已经达到千万级别. 整体验证方法由于超出内存无法得
出验证结果, 而我们的组合验证方法可以进行验证并得出其验证耗费时间, 最大为 247 136 ms. 这充分说明我们的

5.3 讨 论
本文提出了一种复杂嵌入式系统需求的一致性组合验证方法. 经过案例研究和方法评估, 我们发现它确实可
行并且有效, 能够有效约减验证系统的状态空间, 特别是应对复杂嵌入式系统, 达成了预计目标. 但是, 我们也意识
到本文方法存在如下限制.
首先, 本文方法建立在问题框架方法基础上, 其需求依赖关系的识别与问题图密切相关. 实际上需求依赖关系
并不限制表示方法, 只要是子需求之间, 就有可能出现数据依赖和控制依赖. 其他的表示方法 (如顺序图), 也能挖
掘数据依赖和控制依赖, 但可能比问题图要复杂, 因为问题图中对问题领域如词法领域和设备进行了明确的分类.