《表1 核安全级仪控系统控制算法》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《一种安全关键软件系统符号执行优化方法》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

安全关键软件耦合现象广泛存在于此领域的各种软件系统中。实验选取较为典型的核安全级仪控系统控制算法的功能模块，从每个模块中选取和其他模块存在耦合性的路径约束，算法块和耦合约束图模型统计信息如表1所示。实验工具为KLEE、CVC4和Z3[23]约束求解器，其中，KLEE是学术界和工业界较为成熟的符号执行工具，CVC4[24]和Z3是学术界和工业界表现较好的约束求解器。实验对比了使用传统的符号执行工具KLEE+CVC4、KLEE+Z3求解器和使用KLEE+优化算法+CVC4、KLEE+优化算法+Z3所体现的求解时间上的优势。对比实验结果如表2所示，时间对比如图4所示，分割后约束可满足性如表3所示。从图4可以看出，M1在不进行符号约束优化的情况下，CVC4所消耗的时间为53 ms，Z3所消耗的时间为34 ms。M4在不进行符号约束优化的情况下，CVC4所消耗的时间为113 ms，Z3所消耗的时间为86 ms。M1使用优化算法后，CVC4求解的时间为35 ms，Z3求解时间为28 ms，求解的时间平均减少了25.80%。对于长约束M4，CVC4和Z3所用时间分别为113 ms和86 ms，优化后所用时间分别为101 ms和74 ms，求解时间平均减少了12.28%。M1～M4的平均求解时间减少了19.18%。大型系统通常会存在大量的这类约束耦合公式，处理多条路径约束时间上会显著减少。从表3可满足性数据看出，由于考虑了变量在子公式出现的频率，常量替换后的约束公式可满足性比较接近直接求解。通过实验对比可以看到，带权最小割集优化分割一方面提高了约束求解的速度，另一方面也提高了约束分割后的可解性。