参数化系统安全性的启发式符号验证

作者：杨秋松; 李明树

来源：软件学报, 2009, (06): 1444-1456.

• 参数化系统
• 安全性
• 向上封闭集合
• 启发式搜索
• 符号验证 parameterized system
• safety property
• upward-closed set
• heuristic search
• symbolic verification

参数化系统(paramterized system)是指包含特定有限状态进程多个实例的并发系统,其中的参数是指系统内进程实例的数目,即系统的规模.反向可达性分析(backward reachability analysis)已被广泛用于验证参数化系统是否满足以向上封闭(upward-closed)集合表示的安全性(safety property).与有限状态系统验证相类似,参数化系统的验证同样也面临着状态爆炸(state explosion)问题,并且模型检测算法的有效性依赖于如何采用有效的数据结构表示状态集合.针对表示无穷状态的向上封闭集合,研究人员提出了多种基于约束(constraint-...

• 单位
  中国科学院研究生院; 中国科学院软件研究所; 计算机科学国家重点实验室