基于吴方法的符号模型检验

• 作者: 曾琼 魏乐 黄健
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 符号模型检验 吴方法 特征列
• 年，卷（期）: 2008,（27）
• 所属期刊栏目: 理论研究
• 页码范围: 46-48,64
• 页数: 4页
• 分类号: TP301
• 字数: 4149字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2008.27.015

摘要

模型检验技术广泛应用于验证并发系统的性质.它的瓶颈一直是内存爆炸问题,将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题.然而,随着系统规模的增大,BDD的大小仍呈指数增长.吴方法是一种处理多项式的符号计算方法,能有效地求解代数方程组并成功地应用于几何定理机器证明.给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法,从而实现对较大规模的系统性质的验证,进一步缓和状态组合爆炸问题.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄健	成都信息工程学院计算机系	20	177	6.0	13.0
5	魏乐	成都信息工程学院计算机系	36	261	9.0	15.0
9	曾琼	成都信息工程学院计算机基础教学部	7	7	2.0	2.0