期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
1
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
模型检验中对CTL公式的空属性探测
被引量:
1
1
作者
郭建
金乃咏
《西安电子科技大学学报》
EI
CAS
CSCD
北大核心
2007年第5期794-799,共6页
在模型检验中建立了一种新方法:检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性.根据原子命题的极性,用TRUE或FALSE替换原子命题,得到一系列的CTL公式,再对这些CTL公式用模型检验工具验证,若CTL公式中有一个通过了验证,则可得...
在模型检验中建立了一种新方法:检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性.根据原子命题的极性,用TRUE或FALSE替换原子命题,得到一系列的CTL公式,再对这些CTL公式用模型检验工具验证,若CTL公式中有一个通过了验证,则可得出该系统属性是一个空属性.该方法对CTL公式的空属性的探测不需要对它的所有子公式用TRUE或FALSE替换,只需对原子命题替换,这样检验的次数与原子命题的个数呈线性关系.利用验证综合系统对十字路口交通控制器规范的空属性进行了检验.
展开更多
关键词
模型检验
空属性探测
可计算时态逻辑公式
验证综合系统系统
下载PDF
职称材料
题名
模型检验中对CTL公式的空属性探测
被引量:
1
1
作者
郭建
金乃咏
机构
西安电子科技大学微电子学院
华东师范大学软件学院
出处
《西安电子科技大学学报》
EI
CAS
CSCD
北大核心
2007年第5期794-799,共6页
基金
国家自然科学基金重大项目资助(90607008)
陕西省教育厅自然科学基金资助(07JK373)
文摘
在模型检验中建立了一种新方法:检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性.根据原子命题的极性,用TRUE或FALSE替换原子命题,得到一系列的CTL公式,再对这些CTL公式用模型检验工具验证,若CTL公式中有一个通过了验证,则可得出该系统属性是一个空属性.该方法对CTL公式的空属性的探测不需要对它的所有子公式用TRUE或FALSE替换,只需对原子命题替换,这样检验的次数与原子命题的个数呈线性关系.利用验证综合系统对十字路口交通控制器规范的空属性进行了检验.
关键词
模型检验
空属性探测
可计算时态逻辑公式
验证综合系统系统
Keywords
model checking
vacuity detection
CTL formula
VIS system
分类号
TP301.1 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
模型检验中对CTL公式的空属性探测
郭建
金乃咏
《西安电子科技大学学报》
EI
CAS
CSCD
北大核心
2007
1
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部