期刊导航
期刊开放获取
cqvip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
1
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
用模型检验产生安全性质的测试
被引量:
1
1
作者
曾红卫
缪淮扣
《应用科学学报》
EI
CAS
CSCD
北大核心
2011年第5期529-536,共8页
安全关键系统必须满足规定的安全性质.测试生成通常独立于给定性质,"先验证再测试"的方法不能保证安全性质被测试.为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法.用输出变异建立被测实现的输出-完全模型,...
安全关键系统必须满足规定的安全性质.测试生成通常独立于给定性质,"先验证再测试"的方法不能保证安全性质被测试.为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法.用输出变异建立被测实现的输出-完全模型,通过发现危险迹产生测试用例.给出了基于图结构覆盖的安全性质测试准则,提出了形式化测试准则的方法.使用模型检验器NuSMV检验输出-完全模型可产生既满足结构覆盖又与安全性质相关的测试用例.
展开更多
关键词
安全性质
模型检验
测试生成
危险
迹
下载PDF
职称材料
题名
用模型检验产生安全性质的测试
被引量:
1
1
作者
曾红卫
缪淮扣
机构
上海大学计算机工程与科学学院
上海市计算机软件评测重点实验室
出处
《应用科学学报》
EI
CAS
CSCD
北大核心
2011年第5期529-536,共8页
基金
国家自然科学基金(No.60970007
No.61073050)
+2 种基金
上海市自然科学基金(No.09ZR1412100)
上海市科学技术委员会项目基金(No.10510704900)
上海市重点学科建设项目基金(No.J50103)资助
文摘
安全关键系统必须满足规定的安全性质.测试生成通常独立于给定性质,"先验证再测试"的方法不能保证安全性质被测试.为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法.用输出变异建立被测实现的输出-完全模型,通过发现危险迹产生测试用例.给出了基于图结构覆盖的安全性质测试准则,提出了形式化测试准则的方法.使用模型检验器NuSMV检验输出-完全模型可产生既满足结构覆盖又与安全性质相关的测试用例.
关键词
安全性质
模型检验
测试生成
危险
迹
Keywords
safety property, model checking, test generation, dangerous trace
分类号
TP311.5 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
用模型检验产生安全性质的测试
曾红卫
缪淮扣
《应用科学学报》
EI
CAS
CSCD
北大核心
2011
1
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部