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

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

最后, 我们整理了所有的案例和验证数据, 结果如表 6 所示. 对于验证结果中涉及的状态空间, 选取整体遍历
状态空间最大的一个性质的验证数据. 这是因为对于不同的验证性质, 它们可以并发执行. 特别地, 对于组合验证,
我们选取同一性质的验证结果中最大状态空间以及最大耗费时间, 这里最大耗费时间是选取对应案例实验中所有
需求进行组合验证中某个需求所对应的最大验证时间, 并不是对应案例中组合验证中所有需求对应的验证时间总
和, 其他具体结果如图 14 所示. 对于整体验证来说, 验证结果记录整体验证的综合结果, 若所有性质都满足一致
性, 则为“满足”, 若存在不满足一致性, 则为“不满足”, 若存在性质超出内存无法验证, 则为“超出内存” (out of
memory). 对于超出内存的情况其最大状态空间和最大耗费时间也无法得知, 一般认为验证状态空间过大导致无
法得出验证结果, 使用“－”代表. 组合验证列中的依赖关系表明了该案例中存在的数据依赖和控制依赖数量. 组合
验证列中的可执行验证子系统指的是根据需求依赖进行组合验证所划分的子系统个数, 而真正执行 NTA 则是与
待验证性质相关需要运行的子系统. 子系统验证结果表明各个子系统验证结果情况. 整体模型验证列中可执行验
证模型代表该案例中软件构件 TA 和设备构件 TA 数量之和, 即需求数量与设备数量之和. 另外, 考虑到操作系统
等因素可能对实验结果产生影响, 我们在实验过程中对每组实验进行了 10 次验证. 我们取这 10 次验证的平均值,
以此来确定最终的探索状态数和所需时间. 其结果如表 6 和图 14 所示. 需要说明的是, 图 14 中的白色柱状展示了
不同验证子系统的状态空间. 参与验证的子系统数量会根据其涉及的验证性质有所不同. 如果某个验证子系统并
未涉及到特定的验证性质中的设备, 那么这个子系统就不会参与到验证过程中. 因此, 状态空间的数量并不一定会
与表 6 中列出的验证子系统数量完全一致.

表 6 组合验证评价结果

案例 本文方法 整体模型验证
状态空间 时间耗费
#可执行 #可执
#需 #设 子系统验 #探索的 最大耗费 验证 #探索的 耗费时 约减比例 约减比例
名称 #依赖关系 验证子 行验证
求 备 证结果 最大状态 时间 (s) 结果 状态 间 (s) (%) (%)
系统 模型
灯光控制 6 5 数据依赖: 3 6 5满足 79 0 11 不满足 143 0 44.76 0
系统 控制依赖: 2 1不满足
智能家居控 11 15 数据依赖: 5 11 9满足 517 955 5.875 26 不满足 697 901 7.812 25.78 24.80
制子系统 2不满足
轨道交通控 4 7 数据依赖: 2 4 4满足 54 0 11 满足 78 0 30.77 0
制子系统 20
机载侦查子 19 12 数据依赖: 11 19 16满足 18 025 481 100.094 31 超出 － － － －
系统 控制依赖: 6 3不满足 内存
太阳搜索控 19 28 数据依赖: 16 15 10满足 19 199 651 247.236 47 超出 － － － －
制子系统 控制依赖: 5 5不满足 内存
注: 符号#标注的列数据可以重点关注

160 800 000 90
143 697 901 78
700 000 80
120 600 000 70
517 955
60 54
500 000
状态空间 80 79 状态空间 400 000 336 618 状态空间 50 34
40
300 000
30 29
40 200 000 17
20
15
100 000 10
0 0 0
组合验证 整体验证 组合验证 整体验证 组合验证 整体验证
状态空间 状态空间 状态空间 状态空间 状态空间 状态空间
(a) 灯光控制系统 (b) 智能家居控制子系统 (c) 轨道交通控制子系统
图 14 各案例组合验证与整体验证状态数对比结果