并发系统模型检测中的状态约减算法
组合可达性分析是对并发系统模型分析验证的基础和关键,但是难于解决验证中的所谓的状态爆炸问题.对此提出了基于假定状态约减验证算法(ABSR),通过自动构造子系统接口定义来约束其状态规模,在验证过程中约减冗余状态,能更大程度降低状态爆炸几率和提高验证效率.借助假定一保证(Assume-Guarantee)算法有效性定理和组合可达性分析(CRA)算法安全性验证定理,证明该验证算法的有效性.通过采用通信系统演算(CCS)描述的任务模型为例证,证明上述算法比传统CRA算法更有效.
并发系统 模型分析 组合可达性 状态约减算法 安全性
陈晓江 杨琛 冯健 房鼎益
西北大学,信息学院,陕西,西安,710127
国内会议
南宁
中文
81-84
2007-10-12（万方平台首次上网日期，不代表论文的发表时间）