基于组合IIS路径抽取的组合线性混成系统有界可达性分析优化

混成系统是一类同时具有离散和连续行为的复杂系统,被广泛应用于控制系统建模.针对其安全性需求,对不安全状态进行有界可达性验证,是保障系统安全的重要手段.然而,当前技术所能处理的问题规模和现实生活里的实际需要尚有一定的距离.特别是组合混成系统由于涉及到各个组件间的协作与同步,组合状态空间快速爆炸,对其进行验证具有极高的复杂性.为控制问题的复杂度,一种面向路径的可达性分析方法在前期工作中被提出用来对组合线性混成系统进行有界可达性分析.该方法通过依次枚举潜在路径并进行验证的方式,有效地提升了所能处理的问题规模.当面对复杂系统时,上述面向路径的检测方法将会因为待检测路径数量的急剧上升而使得验证效率大幅降低,这也是模型检验状态空间爆炸问题的一种体现.为解决此问题,本文提出了一种状态空间约减技术以加速验证过程.当一组路径被判定为不可行时,定位出导致其不可行的原因,得到一个组合不可行路径片段.由于包含同样片段的组合路径一定不可行,因此在后续的路径遍历里只需要枚举与检验不包含组合不可行路径片段的路径,从而大幅减少需要检验的路径数量.此外,为了有效地规避此类组合路径片段,我们设计了一种全新的基于SMT编码的有界图结构遍历方法.实验表明,该优化技术大幅地提升了面向路径有界可达性分析方法的性能,整体性能也超越了当前最先进的同类工具.