公开(公告)号：CN104267936B

公开(公告)日：2017-10-17

申请号：CN201410470378.8

申请日：2014-09-16

Applicant: 桂林电子科技大学

Inventor： 钱俊彦 ,  曾宇清 ,  赵岭忠 ,  郭云川 ,  李凤英

IPC: G06F9/44

Abstract: 基于树语义的异步动态下推网络可达性分析方法属于软件安全、可靠性技术领域，其特征在于将树语义引入到异步动态下推网络中，通过构建一个中间模型模拟模型的树语义，并采用上下文限界方法使模型的可达性为可判定，计算有限的k次上下文执行内的可达格局集合，通过计算可达格局集合与目标格局集合的交集是否为空，判断出目标格局集合是否可达，从而确定程序的抽象模型中是否存在设计错误或漏洞，保证模型的正确与可靠。

公开(公告)号：CN104267936A

公开(公告)日：2015-01-07

申请号：CN201410470378.8

申请日：2014-09-16

Applicant: 桂林电子科技大学

Inventor： 钱俊彦 ,  曾宇清 ,  赵岭忠 ,  郭云川 ,  李凤英

IPC: G06F9/44

Abstract: 基于树语义的异步动态下推网络可达性分析方法属于软件安全、可靠性技术领域，其特征在于将树语义引入到异步动态下推网络中，通过构建一个中间模型模拟模型的树语义，并采用上下文限界方法使模型的可达性为可判定，计算有限的k次上下文执行内的可达格局集合，通过计算可达格局集合与目标格局集合的交集是否为空，判断出目标格局集合是否可达，从而确定程序的抽象模型中是否存在设计错误或漏洞，保证模型的正确与可靠。