期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
1
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
并发系统模型检测中的状态约减算法
1
作者
陈晓江
杨琛
+1 位作者
冯健
房鼎益
《微电子学与计算机》
CSCD
北大核心
2007年第10期81-84,共4页
组合可达性分析是对并发系统模型分析验证的基础和关键,但是难于解决验证中的所谓的状态爆炸问题。对此提出了基于假定状态约减验证算法(ABSR),通过自动构造子系统接口定义来约束其状态规模,在验证过程中约减冗余状态,能更大程度降低状...
组合可达性分析是对并发系统模型分析验证的基础和关键,但是难于解决验证中的所谓的状态爆炸问题。对此提出了基于假定状态约减验证算法(ABSR),通过自动构造子系统接口定义来约束其状态规模,在验证过程中约减冗余状态,能更大程度降低状态爆炸几率和提高验证效率。借助假定-保证(Assume-Guarantee)算法有效性定理和组合可达性分析(CRA)算法安全性验证定理,证明该验证算法的有效性。通过采用通信系统演算(CCS)描述的任务模型为例证,证明上述算法比传统CRA算法更有效。
展开更多
关键词
通信系统演算
模型检测
组合可达性分析
状态爆炸
假定一保证算法
安全性
下载PDF
职称材料
题名
并发系统模型检测中的状态约减算法
1
作者
陈晓江
杨琛
冯健
房鼎益
机构
西北大学信息学院
出处
《微电子学与计算机》
CSCD
北大核心
2007年第10期81-84,共4页
基金
航空科学基金项目(03F31007)
陕西省国际合作项目(2006kw-21)
+1 种基金
陕西省自然科学基金项目(2007F06)
西北大学科研基金项目(04NW41)
文摘
组合可达性分析是对并发系统模型分析验证的基础和关键,但是难于解决验证中的所谓的状态爆炸问题。对此提出了基于假定状态约减验证算法(ABSR),通过自动构造子系统接口定义来约束其状态规模,在验证过程中约减冗余状态,能更大程度降低状态爆炸几率和提高验证效率。借助假定-保证(Assume-Guarantee)算法有效性定理和组合可达性分析(CRA)算法安全性验证定理,证明该验证算法的有效性。通过采用通信系统演算(CCS)描述的任务模型为例证,证明上述算法比传统CRA算法更有效。
关键词
通信系统演算
模型检测
组合可达性分析
状态爆炸
假定一保证算法
安全性
Keywords
calculus of communicating system
model-checking
,
compositional reaehability analysis
state explosion
assume-guarantee reasoning
safety property
分类号
TP338.6 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
并发系统模型检测中的状态约减算法
陈晓江
杨琛
冯健
房鼎益
《微电子学与计算机》
CSCD
北大核心
2007
0
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部