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