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

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