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

发布时间：2019-03-25 21:22

【摘要】：混成系统是一类同时具有离散和连续行为的复杂系统,被广泛应用于控制系统建模.针对其安全性需求,对不安全状态进行有界可达性验证,是保障系统安全的重要手段.然而,当前技术所能处理的问题规模和现实生活里的实际需要尚有一定的距离.特别是组合混成系统由于涉及到各个组件间的协作与同步,组合状态空间快速爆炸,对其进行验证具有极高的复杂性.为控制问题的复杂度,一种面向路径的可达性分析方法在前期工作中被提出用来对组合线性混成系统进行有界可达性分析.该方法通过依次枚举潜在路径并进行验证的方式,有效地提升了所能处理的问题规模.当面对复杂系统时,上述面向路径的检测方法将会因为待检测路径数量的急剧上升而使得验证效率大幅降低,这也是模型检验状态空间爆炸问题的一种体现.为解决此问题,本文提出了一种状态空间约减技术以加速验证过程.当一组路径被判定为不可行时,定位出导致其不可行的原因,得到一个组合不可行路径片段.由于包含同样片段的组合路径一定不可行,因此在后续的路径遍历里只需要枚举与检验不包含组合不可行路径片段的路径,从而大幅减少需要检验的路径数量.此外,为了有效地规避此类组合路径片段,我们设计了一种全新的基于SMT编码的有界图结构遍历方法.实验表明,该优化技术大幅地提升了面向路径有界可达性分析方法的性能,整体性能也超越了当前最先进的同类工具.
[Abstract]:Hybrid system is a kind of complex system with both discrete and continuous behavior. It is widely used in the modeling of control systems. According to its security requirements, it is an important means to ensure the security of the system to verify the reachability of the insecure state. However, there is still a certain distance between the scale of the problems that the current technology can deal with and the actual needs of the real life. Especially, it is very complicated to verify the combinatorial hybrid system because it involves the cooperation and synchronization among the components and explodes rapidly in the combinatorial state space. In order to control the complexity of the problem, a path-oriented reachability analysis method was proposed in the previous work to analyze the bounded reachability of composite linear hybrid systems. By enumerating and validating the potential paths in turn, this method can effectively increase the size of the problem that can be dealt with. When faced with complex systems, the above-mentioned path-oriented detection methods will greatly reduce the verification efficiency due to the sharp increase in the number of paths to be detected, which is also a manifestation of the state space explosion problem of model checking. In order to solve this problem, a state space reduction technique is proposed to accelerate the verification process. When a group of paths is determined to be infeasible, the reasons leading to its infeasibility are located, and a combined infeasible path fragment is obtained. Since a combinatorial path containing the same fragment must not be feasible, it is necessary to enumerate and verify the paths that do not contain the combinatorial infeasible path fragment in the subsequent path traversal, thus greatly reducing the number of paths that need to be checked. In addition, in order to avoid this kind of combinatorial path fragments effectively, we design a new traversal method of bounded graph structure based on SMT coding. The experimental results show that the optimization technique greatly improves the performance of the path-oriented bounded reachability analysis method, and the overall performance exceeds the most advanced tools of the same kind.
【作者单位】：南京大学计算机软件新技术国家重点实验室;江苏省软件新技术与产业化协同创新中心;
【基金】：国家重点基础研究发展计划(973)(批准号:2014CB340703) 国家自然科学基金(批准号:61561146394,61572249,61321491)资助项目
【分类号】：TP301.1

【相似文献】