文献类型：期刊文章

作　　者：陈睿[1,2] 杨孟飞[3] 郭向英[1,2]

机构地区：[1]北京控制工程研究所,北京100190 [2]北京轩宇信息技术有限公司,北京100190 [3]中国空间技术研究院,北京100094

出　　处：《软件学报》

基　　金：国家自然科学基金(91118007)~~

年　　份：2016

卷　　号：27

期　　号：3

起止页码：547-561

语　　种：中文

收录情况：AJ、BDHX、BDHX2014、CSA、CSA-PROQEUST、CSCD、CSCD2015_2016、EI(收录号：20161902371609)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、ZMATH、核心刊

摘　　要：在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而,中断在并发语义、同步机制、调度机制等方面与线程(任务)有诸多不同,具有Ad-hoc特征,难以统一刻画,因此,主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争案例库为基础进行了系统分析,提出刻画有害中断数据竞争的7种缺陷模式.针对其中最常见且最难解决的单变量访问序模式,基于抽象解释,提出一种支持过程间分析、中断并发分析的高效检测方法.设计并实现了相应的检测工具Space DRC.实验结果表明,Space DRC能够在145ms内检测出约21 400行程序中的真实数据竞争.Space DRC已经在多个航天重点型号中进行了应用,使得中断数据竞争专项分析的效率提高了至少5倍,并且降低了问题遗漏率.

关 键 词：中断驱动型程序  数据竞争 抽象解释  

分 类 号：TP311]