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

• 作者: 徐力 钱俊彦
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: 动态下推网络 k-定界 可达性分析 符号化
• 年，卷（期）: 2016,（1）
• 页码范围: 48-51
• 页数: 4页
• 分类号: TP301
• 字数: 3852字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	钱俊彦	桂林电子科技大学计算机科学与工程学院	86	238	9.0	10.0
2	徐力	桂林电子科技大学计算机科学与工程学院	2	1	1.0	1.0