期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
3
篇文章
<
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
职称材料
优化基于模型检验的测试生成
被引量:
2
2
作者
曾红卫
缪淮扣
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2011年第3期496-502,共7页
利用模型检验器输出的反例构造测试用例是测试自动化的一种重要手段.由于一个测试用例可能覆盖多个测试目标,测试生成过程中可能存在不必要的对模型检验器的调用,测试包也往往存在大量冗余,严重影响测试性能.为此,提出一种测试生成的动...
利用模型检验器输出的反例构造测试用例是测试自动化的一种重要手段.由于一个测试用例可能覆盖多个测试目标,测试生成过程中可能存在不必要的对模型检验器的调用,测试包也往往存在大量冗余,严重影响测试性能.为此,提出一种测试生成的动态监控优化方法.在模型检验一个测试目标产生测试用例后,采用时态逻辑公式重写技术缩减测试目标集,删除那些被新测试用例覆盖的测试目标;同时,在新测试用例加入测试包时对其进行筛选,以消除冗余.实例结果表明,文中方法可有效地减少模型检验器的调用次数,缩减测试包.
展开更多
关键词
模型检验
测试用例生成
时态逻辑公式
重写
测试包缩减
下载PDF
职称材料
基于模型检查的XML Schema特征提取
被引量:
5
3
作者
刘科
杨红丽
+2 位作者
廖湖声
吕关锋
高雁飞
《计算机应用与软件》
CSCD
北大核心
2012年第11期160-164,共5页
XQuery用于查询XML文档,对XQuery查询优化有助于提高查询效率,有重要的研究意义。树模式把XQuery表示成树结构的查询,如何基于XML Schema对树模式进行优化是当前的研究热点,需要利用XML Schema的一些特征进行树模式优化,因此如何自动提...
XQuery用于查询XML文档,对XQuery查询优化有助于提高查询效率,有重要的研究意义。树模式把XQuery表示成树结构的查询,如何基于XML Schema对树模式进行优化是当前的研究热点,需要利用XML Schema的一些特征进行树模式优化,因此如何自动提取XML Schema的特征是需要解决的问题。提出基于模型检查的XML Schema特征提取方法。首先把XML Schema转换成Schema图,进而转换成模型检查器NuSMV的输入模型,从而可以对时态逻辑公式表示的XML Schema特征进行检查,提取的孩子关系以及子孙关系特征可以用于树模式优化。
展开更多
关键词
模型检查
时态逻辑公式
XML
SCHEMA
Schema特征
下载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
职称材料
题名
优化基于模型检验的测试生成
被引量:
2
2
作者
曾红卫
缪淮扣
机构
上海大学计算机工程与科学学院
出处
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2011年第3期496-502,共7页
基金
国家自然科学基金(60970007
61073050)
+2 种基金
上海市自然科学基金(09ZR1412100)
上海市科学技术委员会项目(10510704900)
上海市重点学科建设项目资助(J50103)
文摘
利用模型检验器输出的反例构造测试用例是测试自动化的一种重要手段.由于一个测试用例可能覆盖多个测试目标,测试生成过程中可能存在不必要的对模型检验器的调用,测试包也往往存在大量冗余,严重影响测试性能.为此,提出一种测试生成的动态监控优化方法.在模型检验一个测试目标产生测试用例后,采用时态逻辑公式重写技术缩减测试目标集,删除那些被新测试用例覆盖的测试目标;同时,在新测试用例加入测试包时对其进行筛选,以消除冗余.实例结果表明,文中方法可有效地减少模型检验器的调用次数,缩减测试包.
关键词
模型检验
测试用例生成
时态逻辑公式
重写
测试包缩减
Keywords
model checking
test case generation
temporal logic formula rewriting
test suite reduction
分类号
TP311.5 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于模型检查的XML Schema特征提取
被引量:
5
3
作者
刘科
杨红丽
廖湖声
吕关锋
高雁飞
机构
北京工业大学
北京建筑工程学院
出处
《计算机应用与软件》
CSCD
北大核心
2012年第11期160-164,共5页
基金
北京市自然科学基金项目(4082003)
中科院软件所项目(40007012201106)
北京市教育委员会科研计划面上项目(KM201010016003)
文摘
XQuery用于查询XML文档,对XQuery查询优化有助于提高查询效率,有重要的研究意义。树模式把XQuery表示成树结构的查询,如何基于XML Schema对树模式进行优化是当前的研究热点,需要利用XML Schema的一些特征进行树模式优化,因此如何自动提取XML Schema的特征是需要解决的问题。提出基于模型检查的XML Schema特征提取方法。首先把XML Schema转换成Schema图,进而转换成模型检查器NuSMV的输入模型,从而可以对时态逻辑公式表示的XML Schema特征进行检查,提取的孩子关系以及子孙关系特征可以用于树模式优化。
关键词
模型检查
时态逻辑公式
XML
SCHEMA
Schema特征
Keywords
Model checking Temporal logic formula XML Schema Schema constraints
分类号
TP391 [自动化与计算机技术—计算机应用技术]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
模型检验中对CTL公式的空属性探测
郭建
金乃咏
《西安电子科技大学学报》
EI
CAS
CSCD
北大核心
2007
1
下载PDF
职称材料
2
优化基于模型检验的测试生成
曾红卫
缪淮扣
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2011
2
下载PDF
职称材料
3
基于模型检查的XML Schema特征提取
刘科
杨红丽
廖湖声
吕关锋
高雁飞
《计算机应用与软件》
CSCD
北大核心
2012
5
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部