期刊导航
期刊开放获取
唐山市科学技术情报研究..
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
5
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式：
文摘
详细
列表
相关度排序
被引量排序
时效性排序
基于多样性SAT求解器和新颖性搜索的软件产品线测试
1
作者
向毅
黄翰
+1 位作者
罗川
杨晓伟
《软件学报》
EI
CSCD
北大核心
2024年第6期2821-2843,共23页
软件产品线测试是一项非常具有挑战性的工作.基于相似性的测试方法通过提升测试集的多样性以达到提高测试覆盖率和缺陷检测率的目的.因其具有良好的可拓展性和较好的测试效果,目前已成为软件产品线测试的重要手段之一.在该测试方法中,...
软件产品线测试是一项非常具有挑战性的工作.基于相似性的测试方法通过提升测试集的多样性以达到提高测试覆盖率和缺陷检测率的目的.因其具有良好的可拓展性和较好的测试效果,目前已成为软件产品线测试的重要手段之一.在该测试方法中,如何产生多样化的测试用例和如何维护测试集的多样性是两个关键问题.针对以上问题,提出一种基于多样性可满足性(SAT)求解器和新颖性搜索(novelty search,NS)的软件产品线测试算法.具体地,所提算法同时采用两类多样性SAT求解器产生多样化的测试用例.特别地,为了改善随机局部搜索SAT求解器的多样性,提出一种基于概率向量的通用策略产生候选解.此外,为同时维护测试集的全局和局部多样性,设计并运用两种基于NS算法思想的归档策略.在50个真实软件产品线上的消融和对比实验验证多样性SAT求解器和两种归档策略的有效性,以及所提算法较其他主流算法的优越性.
展开更多
关键词
软件产品线测试
可满足性求解器
新颖
性
搜索
在线阅读
下载PDF
职称材料
基于可满足性模理论求解器的程序路径验证方法
被引量：
2
2
作者
任胜兵
吴斌
+1 位作者
张健威
王志健
《计算机应用》
CSCD
北大核心
2016年第10期2806-2810,共5页
针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论(SMT)求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式,构造...
针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论(SMT)求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式,构造无循环控制流图(NLCFG);然后通过基本路径法对控制流图(CFG)进行遍历,提取基本路径信息;最后利用SMT求解器作为约束求解器,将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比,该方法在对测试集程序的验证时间上比CBMC降低了25%以上,比FSoft-SMT降低了15%以上;在验证精度上,该方法有明显的提升。实验结果表明,方法可以有效解决路径搜索空间过大的问题,同时提高路径验证的效率和准确率。
展开更多
关键词
路径验证
控制流图
决策树
基本路径
可满足
性
模理论
求解
器
在线阅读
下载PDF
职称材料
语义标识的过程模型的可执行性分析
3
作者
龚平
蒋建明
张仕
《小型微型计算机系统》
CSCD
北大核心
2012年第12期2618-2624,共7页
语义标识的过程模型是基于领域本体对过程模型中活动的前置条件&效果进行标识后所产生的模型.语义过程模型的可执行性问题是确保语义过程模型质量的核心问题,同时已被证明是一个co-NP难问题.基于关联变量集模型定义了语义过程模型...
语义标识的过程模型是基于领域本体对过程模型中活动的前置条件&效果进行标识后所产生的模型.语义过程模型的可执行性问题是确保语义过程模型质量的核心问题,同时已被证明是一个co-NP难问题.基于关联变量集模型定义了语义过程模型的动态语义;定义了该动态语义的命题公式的编码规则;提出了基于可满足性求解器的可执行性分析方法;该方法能判定可执行性问题同时当模型不满足可执行性时能反馈出有问题的活动;此外,实现了相应的原型工具SPMT,该工具支持对语义过程模型的建模及可执行性分析;最后通过实际例子对以上理论及工具进行了有效性验证.
展开更多
关键词
语义标注过程模型
可执行
性
有界模型检查
可满足性求解器
在线阅读
下载PDF
职称材料
具有约束条件的组合测试用例集的构建方法
被引量：
1
4
作者
丁怀宝
高建华
《计算机工程与设计》
CSCD
北大核心
2010年第14期3189-3192,3206,共5页
针对如何为存在约束条件的软件系统生成尽可能小的组合测试用例集问题,提出了基于组合测试算法的约束组合测试法。该方法是对待测系统中的约束条件进行处理,将约束条件先转化为合取范式再转化为布尔表达式的形式。利用布尔可满足性求解...
针对如何为存在约束条件的软件系统生成尽可能小的组合测试用例集问题,提出了基于组合测试算法的约束组合测试法。该方法是对待测系统中的约束条件进行处理,将约束条件先转化为合取范式再转化为布尔表达式的形式。利用布尔可满足性求解器进行求解,找出满足约束条件的约束组合测试用例。最后运用AETG-SAT算法得到较优的组合测试用例集,并通过实验表明了AETG-SAT算法的优越性。
展开更多
关键词
组合测试
约束条件
合取范式
布尔表达式
可满足性求解器
在线阅读
下载PDF
职称材料
Spark环境下基于SMT的分布式限界模型检测
5
作者
任胜兵
张健威
+1 位作者
吴斌
王志健
《计算机工程》
CAS
CSCD
北大核心
2017年第6期19-23,29,共6页
在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布...
在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示(LLVM-IR)构造为Spark内置的数据结构Pair RDD,利用MapReduce算法将Pair RDD转化为表示验证条件的弹性分布式数据集(VCs RDD),VCs RDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明,与传统串行检测方法相比,该方法提高了验证过程中的限界深度和验证结果的正确率,并且对于复杂度较高的程序在限界相同的情况下其验证速度也有所提升。
展开更多
关键词
软件验证
限界模型检测
弹
性
分布式数据集
可满足
性
模理论
求解
器
Spark框架
在线阅读
下载PDF
职称材料
题名
基于多样性SAT求解器和新颖性搜索的软件产品线测试
1
作者
向毅
黄翰
罗川
杨晓伟
机构
华南理工大学软件学院
北京航空航天大学软件学院
出处
《软件学报》
EI
CSCD
北大核心
2024年第6期2821-2843,共23页
基金
广东省科技攻关重点项目(2020B0303300001)
2018–2019年度广东省“新一代人工智能”重大项目(2020AAA0108404)
+3 种基金
国家自然科学基金(61906069,62276103,62202025,61876207)
广东省基础与应用基础研究基金(2019A1515011700,2020A1515010696,2022A1515011491)
中央高校基本科研业务费专项资金(2020ZYGXZR014)
广东省财税大数据重点实验室开放基金(2022kyc021)。
文摘
软件产品线测试是一项非常具有挑战性的工作.基于相似性的测试方法通过提升测试集的多样性以达到提高测试覆盖率和缺陷检测率的目的.因其具有良好的可拓展性和较好的测试效果,目前已成为软件产品线测试的重要手段之一.在该测试方法中,如何产生多样化的测试用例和如何维护测试集的多样性是两个关键问题.针对以上问题,提出一种基于多样性可满足性(SAT)求解器和新颖性搜索(novelty search,NS)的软件产品线测试算法.具体地,所提算法同时采用两类多样性SAT求解器产生多样化的测试用例.特别地,为了改善随机局部搜索SAT求解器的多样性,提出一种基于概率向量的通用策略产生候选解.此外,为同时维护测试集的全局和局部多样性,设计并运用两种基于NS算法思想的归档策略.在50个真实软件产品线上的消融和对比实验验证多样性SAT求解器和两种归档策略的有效性,以及所提算法较其他主流算法的优越性.
关键词
软件产品线测试
可满足性求解器
新颖
性
搜索
Keywords
software product line testing
satisfiability solver
novelty search
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
基于可满足性模理论求解器的程序路径验证方法
被引量：
2
2
作者
任胜兵
吴斌
张健威
王志健
机构
中南大学软件学院
出处
《计算机应用》
CSCD
北大核心
2016年第10期2806-2810,共5页
基金
国家自然科学基金资助项目(61272151)
中南大学研究生自主探索创新项目(2016zzts374)~~
文摘
针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论(SMT)求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式,构造无循环控制流图(NLCFG);然后通过基本路径法对控制流图(CFG)进行遍历,提取基本路径信息;最后利用SMT求解器作为约束求解器,将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比,该方法在对测试集程序的验证时间上比CBMC降低了25%以上,比FSoft-SMT降低了15%以上;在验证精度上,该方法有明显的提升。实验结果表明,方法可以有效解决路径搜索空间过大的问题,同时提高路径验证的效率和准确率。
关键词
路径验证
控制流图
决策树
基本路径
可满足
性
模理论
求解
器
Keywords
path validation
Control Flow Graph （CFG）
decision tree
basic path
Satisfiability Modulo Theory （SMT）solver
分类号
TP311.5 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
语义标识的过程模型的可执行性分析
3
作者
龚平
蒋建明
张仕
机构
福建师范大学数学与计算机科学学院
出处
《小型微型计算机系统》
CSCD
北大核心
2012年第12期2618-2624,共7页
基金
国家自然科学基金项目(61100017)资助
福建省自然基金项目(2012J05112)资助
+1 种基金
福建省教育厅A类项目(JA10080
JA11069)资助
文摘
语义标识的过程模型是基于领域本体对过程模型中活动的前置条件&效果进行标识后所产生的模型.语义过程模型的可执行性问题是确保语义过程模型质量的核心问题,同时已被证明是一个co-NP难问题.基于关联变量集模型定义了语义过程模型的动态语义;定义了该动态语义的命题公式的编码规则;提出了基于可满足性求解器的可执行性分析方法;该方法能判定可执行性问题同时当模型不满足可执行性时能反馈出有问题的活动;此外,实现了相应的原型工具SPMT,该工具支持对语义过程模型的建模及可执行性分析;最后通过实际例子对以上理论及工具进行了有效性验证.
关键词
语义标注过程模型
可执行
性
有界模型检查
可满足性求解器
Keywords
semantically annotated process model
executability
bounded model checking
SAT solver
分类号
TP393 [自动化与计算机技术—计算机应用技术]
在线阅读
下载PDF
职称材料
题名
具有约束条件的组合测试用例集的构建方法
被引量：
1
4
作者
丁怀宝
高建华
机构
上海师范大学计算机科学与工程系
出处
《计算机工程与设计》
CSCD
北大核心
2010年第14期3189-3192,3206,共5页
基金
国家自然科学基金项目(60673067)
上海市教育委员会科研创新基金项目(0922135)
上海市科委基金项目(09220503000)
文摘
针对如何为存在约束条件的软件系统生成尽可能小的组合测试用例集问题,提出了基于组合测试算法的约束组合测试法。该方法是对待测系统中的约束条件进行处理,将约束条件先转化为合取范式再转化为布尔表达式的形式。利用布尔可满足性求解器进行求解,找出满足约束条件的约束组合测试用例。最后运用AETG-SAT算法得到较优的组合测试用例集,并通过实验表明了AETG-SAT算法的优越性。
关键词
组合测试
约束条件
合取范式
布尔表达式
可满足性求解器
Keywords
combination testing
constraints
conjunctive normal form
Boolean expression
SAT solver
分类号
TP311.5 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
Spark环境下基于SMT的分布式限界模型检测
5
作者
任胜兵
张健威
吴斌
王志健
机构
中南大学软件学院嵌入式系统与网络实验室
出处
《计算机工程》
CAS
CSCD
北大核心
2017年第6期19-23,29,共6页
基金
国家自然科学基金面上项目(61272151)
中南大学自主探索创新项目(2016zzts373)
文摘
在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示(LLVM-IR)构造为Spark内置的数据结构Pair RDD,利用MapReduce算法将Pair RDD转化为表示验证条件的弹性分布式数据集(VCs RDD),VCs RDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明,与传统串行检测方法相比,该方法提高了验证过程中的限界深度和验证结果的正确率,并且对于复杂度较高的程序在限界相同的情况下其验证速度也有所提升。
关键词
软件验证
限界模型检测
弹
性
分布式数据集
可满足
性
模理论
求解
器
Spark框架
Keywords
software verification
Bounded Model Checking （BMC）
Resilient Distributed Dataset（RDD）
SatisfiablityModulo Theories （SMT） solver
Spark framework
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
基于多样性SAT求解器和新颖性搜索的软件产品线测试
向毅
黄翰
罗川
杨晓伟
《软件学报》
EI
CSCD
北大核心
2024
0
在线阅读
下载PDF
职称材料
2
基于可满足性模理论求解器的程序路径验证方法
任胜兵
吴斌
张健威
王志健
《计算机应用》
CSCD
北大核心
2016
2
在线阅读
下载PDF
职称材料
3
语义标识的过程模型的可执行性分析
龚平
蒋建明
张仕
《小型微型计算机系统》
CSCD
北大核心
2012
0
在线阅读
下载PDF
职称材料
4
具有约束条件的组合测试用例集的构建方法
丁怀宝
高建华
《计算机工程与设计》
CSCD
北大核心
2010
1
在线阅读
下载PDF
职称材料
5
Spark环境下基于SMT的分布式限界模型检测
任胜兵
张健威
吴斌
王志健
《计算机工程》
CAS
CSCD
北大核心
2017
0
在线阅读
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部
