基于自动机的并发程序符号可达分析

作者：曾宇清; 钱俊彦

来源：桂林电子科技大学学报, 2013, (04): 300-304.

• 状态爆炸
• 可达性
• 自动机
• 符号 state explosion
• reachability
• automata technology
• symbol

为了缓解模型检测并发程序中出现的状态爆炸问题,将并发程序建模成异步动态下推网络,同时将异步动态下推网络转化为异步下推网络,在异步下推网络下提出一种基于自动机的符号可达算法。该算法能避免精确搜索每一个状态空间,有效地缓解了状态爆炸。

• 单位
  桂林电子科技大学