基于k-定界的动态下推网络可达性分析

引文格式： 徐力，钱俊彦.基于k-定界的动态下推网络可达性分析[J].桂林电子科技大学学报,2016,36(1):48-51.

徐力，钱俊彦

(桂林电子科技大学 计算机科学与工程学院，广西 桂林541004)

摘要：为了保证含有递归、动态创建线程并发系统的安全性，提出基于动态下推网络模型的形式化验证方法。该模型的可达性为不可判定，把动态下推网络转换为在k-定界下可达性可判定的下推网络，再将转换后的下推网络符号化。分析表明，该方法可使模型可达性成为可判定的，且缓解了模型状态空间爆炸的状态。

关键词：动态下推网络；k-定界；可达性分析；符号化

随着多核技术的发展以及内存容量越来越大，基于充分利用资源的原则，Java语言引入Fork/Join并行模式，通过该模式，并发程序可把线程分解成更细粒度的子线程并行执行[1]，且动态创建新线程[2]对构造系统组件具有重要意义，如在程序执行过程中，可创建新线程，实现函数回调。但由于并发线程交错执行，使得代码中隐匿的漏洞和错误难以检测。

为保证带动态线程创建和含有递归的并发程序运行安全，采用动态下推网络[3]对其进行模型检测。然而，动态下推网络可达性不可判定[4]，使得验证难以实现。Qadeer等[5]提出了k-定界可达算法，解决了多栈下推系统的上下文模型检测，但无法解决带动态线程创建的可达性问题。

鉴于此，基于k-定界技术，将动态下推网络模拟成可达性可判定[6]的下推网络，并基于下推网络提出一种符号下推网络可达算法[7]，压缩状态空间来缓解爆炸问题的状态。……