并发系统模型检测中的状态约减算法

• 作者: 冯健 房鼎益 杨琛 陈晓江
• 来源期刊: 微电子学与计算机
• 关键词: 通信系统演算 模型检测 组合可达性分析 状态爆炸 假定一保证算法 安全性
• 年，卷（期）: 2007,（10）
• 页码范围: 81-84
• 页数: 4页
• 分类号: TP338.6
• 语种: 中文
• DOI: 10.3969/j.issn.1000-7180.2007.10.024

摘要

组合可达性分析是对并发系统模型分析验证的基础和关键,但是难于解决验证中的所谓的状态爆炸问题.对此提出了基于假定状态约减验证算法(ABSR),通过自动构造子系统接口定义来约束其状态规模,在验证过程中约减冗余状态,能更大程度降低状态爆炸几率和提高验证效率.借助假定一保证(Assume-Guarantee)算法有效性定理和组合可达性分析(CRA)算法安全性验证定理,证明该验证算法的有效性.通过采用通信系统演算(CCS)描述的任务模型为例证,证明上述算法比传统CRA算法更有效.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	房鼎益	西北大学信息学院	124	1289	16.0	31.0
2	冯健	西北大学信息学院	9	128	6.0	9.0
3	陈晓江	西北大学信息学院	65	696	13.0	25.0
4	杨琛	西北大学信息学院	2	1	1.0	1.0