期刊导航
期刊开放获取
cqvip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
4
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式：
文摘
详细
列表
相关度排序
被引量排序
时效性排序
基于变量访问序模式的中断数据竞争检测方法
被引量：
17
1
作者
陈睿
杨孟飞
郭向英
《软件学报》
EI
CSCD
北大核心
2016年第3期547-561,共15页
在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而,中断在并发语义、同步机制、调度机制等方面与线程(任务)有诸多不同,具有Ad-hoc特征,难以统一刻画,因此,主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争...
在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而,中断在并发语义、同步机制、调度机制等方面与线程(任务)有诸多不同,具有Ad-hoc特征,难以统一刻画,因此,主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争案例库为基础进行了系统分析,提出刻画有害中断数据竞争的7种缺陷模式.针对其中最常见且最难解决的单变量访问序模式,基于抽象解释,提出一种支持过程间分析、中断并发分析的高效检测方法.设计并实现了相应的检测工具Space DRC.实验结果表明,Space DRC能够在145ms内检测出约21 400行程序中的真实数据竞争.Space DRC已经在多个航天重点型号中进行了应用,使得中断数据竞争专项分析的效率提高了至少5倍,并且降低了问题遗漏率.
展开更多
关键词
中断驱动型程序
数据竞争
抽象解释
下载PDF
职称材料
静态检测中断驱动程序的数据竞争
被引量：
9
2
作者
霍玮
于洪涛
+1 位作者
冯晓兵
张兆庆
《计算机研究与发展》
EI
CSCD
北大核心
2011年第12期2290-2299,共10页
直接运行于微控制器上的中断驱动程序中可能存在一种重要的程序错误:数据竞争.然而当前主流的数据竞争静态检测技术因其服务于多线程模型程序而不适用.设计简明、易用的中断特征描述语言可以使得竞争检测具有平台无关性;同时,提出了一...
直接运行于微控制器上的中断驱动程序中可能存在一种重要的程序错误:数据竞争.然而当前主流的数据竞争静态检测技术因其服务于多线程模型程序而不适用.设计简明、易用的中断特征描述语言可以使得竞争检测具有平台无关性;同时,提出了一个流敏感的、上下文敏感的、考虑中断驱动程序原子性、易变性和部分随机性的数据竞争检测算法.该算法具有高效、精确的特点.实验表明,其检测时间与代码规模基本呈线性关系,分析17850行代码仅用时3.6s;同时,相比于基于锁集技术的典型数据竞争检测方法,其准确率平均是后者的2.13倍.
展开更多
关键词
微控制器
中断驱动程序
数据竞争检测
过程间数据流分析
副作用分析
下载PDF
职称材料
航天嵌入式软件整数溢出的形式化验证方法
被引量：
2
3
作者
高猛
滕俊元
王政
《软件学报》
EI
CSCD
北大核心
2021年第10期2977-2992,共16页
整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检...
整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约简技术;同时,针对中断驱动型程序,结合中断函数特征抽象,提出了基于干扰变量的中断驱动程序顺序化方法.经过基准测试程序和真实航天嵌入式软件实验,结果表明:该方法在保证整数溢出问题检出率的前提下,不仅能够提高分析效率,还使得已有的模型检测技术能够适用于中断驱动型程序整数溢出检测.
展开更多
关键词
航天嵌入式软件
整数溢出
有界模型检测
中断驱动型程序
顺序化
下载PDF
职称材料
航天嵌入式软件数组越界缺陷特征研究
被引量：
1
4
作者
陈睿
于婷婷
+4 位作者
贾春鹏
李超
高栋栋
江云松
杨孟飞
《空间控制技术与应用》
CSCD
北大核心
2021年第2期1-9,共9页
根据统计,数组越界是航天嵌入式软件开发过程中出现最多且最容易被遗漏的缺陷类型之一.目前自动化检测数组越界多基于抽象解释、符号执行、程序模型检验等方法,这些方法在误报、漏报、可扩展性等方面的表现依赖于软件及缺陷特征.分析了...
根据统计,数组越界是航天嵌入式软件开发过程中出现最多且最容易被遗漏的缺陷类型之一.目前自动化检测数组越界多基于抽象解释、符号执行、程序模型检验等方法,这些方法在误报、漏报、可扩展性等方面的表现依赖于软件及缺陷特征.分析了近三年航天嵌入式软件第三方测试中发现的94个数组越界问题,从缺陷模式和缺陷表现形式两方面分析得出10项航天嵌入式软件数组越界缺陷特征,并提出对设计具体检测方法关键的若干启示.进一步基于这些特征和启示探讨了数组越界检测算法针对中断驱动型程序的改进方向.
展开更多
关键词
航天嵌入式软件
数组越界
程序分析
中断驱动型程序
下载PDF
职称材料
题名
基于变量访问序模式的中断数据竞争检测方法
被引量：
17
1
作者
陈睿
杨孟飞
郭向英
机构
北京控制工程研究所
北京轩宇信息技术有限公司
中国空间技术研究院
出处
《软件学报》
EI
CSCD
北大核心
2016年第3期547-561,共15页
基金
国家自然科学基金(91118007)~~
文摘
在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而,中断在并发语义、同步机制、调度机制等方面与线程(任务)有诸多不同,具有Ad-hoc特征,难以统一刻画,因此,主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争案例库为基础进行了系统分析,提出刻画有害中断数据竞争的7种缺陷模式.针对其中最常见且最难解决的单变量访问序模式,基于抽象解释,提出一种支持过程间分析、中断并发分析的高效检测方法.设计并实现了相应的检测工具Space DRC.实验结果表明,Space DRC能够在145ms内检测出约21 400行程序中的真实数据竞争.Space DRC已经在多个航天重点型号中进行了应用,使得中断数据竞争专项分析的效率提高了至少5倍,并且降低了问题遗漏率.
关键词
中断驱动型程序
数据竞争
抽象解释
Keywords
interrupt
-
driven
program
data
race
abstract
interpretation
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
静态检测中断驱动程序的数据竞争
被引量：
9
2
作者
霍玮
于洪涛
冯晓兵
张兆庆
机构
中国科学院计算技术研究所计算机体系结构国家重点实验室(筹)
出处
《计算机研究与发展》
EI
CSCD
北大核心
2011年第12期2290-2299,共10页
基金
国家"八六三"高技术研究发展计划基金项目(2008AA01Z115)
"核高基"国家重大科技专项基金项目(2009ZX01036-001-002)
+1 种基金
国家"九七三"重点基础研究发展计划基金项目(2011CB302504)
国家自然科学基金项目(60921002)
文摘
直接运行于微控制器上的中断驱动程序中可能存在一种重要的程序错误:数据竞争.然而当前主流的数据竞争静态检测技术因其服务于多线程模型程序而不适用.设计简明、易用的中断特征描述语言可以使得竞争检测具有平台无关性;同时,提出了一个流敏感的、上下文敏感的、考虑中断驱动程序原子性、易变性和部分随机性的数据竞争检测算法.该算法具有高效、精确的特点.实验表明,其检测时间与代码规模基本呈线性关系,分析17850行代码仅用时3.6s;同时,相比于基于锁集技术的典型数据竞争检测方法,其准确率平均是后者的2.13倍.
关键词
微控制器
中断驱动程序
数据竞争检测
过程间数据流分析
副作用分析
Keywords
microcontroller
interrupt
-
driven
program
data
race
detection
interprocedural
dataflow
analysis
side-effect
analysis
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
航天嵌入式软件整数溢出的形式化验证方法
被引量：
2
3
作者
高猛
滕俊元
王政
机构
北京控制工程研究所
北京轩宇信息技术有限公司
出处
《软件学报》
EI
CSCD
北大核心
2021年第10期2977-2992,共16页
基金
国家自然科学基金(61802017)
装备预研领域基金(61400020407)。
文摘
整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约简技术;同时,针对中断驱动型程序,结合中断函数特征抽象,提出了基于干扰变量的中断驱动程序顺序化方法.经过基准测试程序和真实航天嵌入式软件实验,结果表明:该方法在保证整数溢出问题检出率的前提下,不仅能够提高分析效率,还使得已有的模型检测技术能够适用于中断驱动型程序整数溢出检测.
关键词
航天嵌入式软件
整数溢出
有界模型检测
中断驱动型程序
顺序化
Keywords
aerospace
embedded
software
integer
overflow
bounded
model
checking
interrupt
-
driven
program
sequentialization
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
航天嵌入式软件数组越界缺陷特征研究
被引量：
1
4
作者
陈睿
于婷婷
贾春鹏
李超
高栋栋
江云松
杨孟飞
机构
北京轩宇信息技术有限公司
北京控制工程研究所
中国空间技术研究院
出处
《空间控制技术与应用》
CSCD
北大核心
2021年第2期1-9,共9页
基金
国家自然科学基金资助项目(61802017)。
文摘
根据统计,数组越界是航天嵌入式软件开发过程中出现最多且最容易被遗漏的缺陷类型之一.目前自动化检测数组越界多基于抽象解释、符号执行、程序模型检验等方法,这些方法在误报、漏报、可扩展性等方面的表现依赖于软件及缺陷特征.分析了近三年航天嵌入式软件第三方测试中发现的94个数组越界问题,从缺陷模式和缺陷表现形式两方面分析得出10项航天嵌入式软件数组越界缺陷特征,并提出对设计具体检测方法关键的若干启示.进一步基于这些特征和启示探讨了数组越界检测算法针对中断驱动型程序的改进方向.
关键词
航天嵌入式软件
数组越界
程序分析
中断驱动型程序
Keywords
aerospace
embedded
software
out-of-bounds
array
access
program
analysis
interrupt
-
driven
program
分类号
TP399 [自动化与计算机技术—计算机应用技术]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
基于变量访问序模式的中断数据竞争检测方法
陈睿
杨孟飞
郭向英
《软件学报》
EI
CSCD
北大核心
2016
17
下载PDF
职称材料
2
静态检测中断驱动程序的数据竞争
霍玮
于洪涛
冯晓兵
张兆庆
《计算机研究与发展》
EI
CSCD
北大核心
2011
9
下载PDF
职称材料
3
航天嵌入式软件整数溢出的形式化验证方法
高猛
滕俊元
王政
《软件学报》
EI
CSCD
北大核心
2021
2
下载PDF
职称材料
4
航天嵌入式软件数组越界缺陷特征研究
陈睿
于婷婷
贾春鹏
李超
高栋栋
江云松
杨孟飞
《空间控制技术与应用》
CSCD
北大核心
2021
1
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部
