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

摘要：

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

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

所属期刊栏目：36

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金61262008;广西自然科学基金2012GXNSFAA053220,2014GXNSFAA118365

在线出版日期：2016-06-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：48-51