【摘要】：在航天嵌入式軟件等中斷驅(qū)動型軟件中,中斷數(shù)據(jù)競爭問題十分突出.然而,中斷在并發(fā)語義、同步機制、調(diào)度機制等方面與線程(任務(wù))有諸多不同,具有Ad-hoc特征,難以統(tǒng)一刻畫,因此,主流的數(shù)據(jù)競爭檢測方法并不適用.以航天嵌入式軟件數(shù)據(jù)競爭案例庫為基礎(chǔ)進行了系統(tǒng)分析,提出刻畫有害中斷數(shù)據(jù)競爭的7種缺陷模式.針對其中最常見且最難解決的單變量訪問序模式,基于抽象解釋,提出一種支持過程間分析、中斷并發(fā)分析的高效檢測方法.設(shè)計并實現(xiàn)了相應(yīng)的檢測工具Space DRC.實驗結(jié)果表明,Space DRC能夠在145ms內(nèi)檢測出約21 400行程序中的真實數(shù)據(jù)競爭.Space DRC已經(jīng)在多個航天重點型號中進行了應(yīng)用,使得中斷數(shù)據(jù)競爭專項分析的效率提高了至少5倍,并且降低了問題遺漏率.
[Abstract]:In space embedded software and other interrupt driven software, interrupt data competition is very prominent. However, interrupt is different from thread (task) in many aspects such as concurrent semantics, synchronization mechanism, scheduling mechanism and so on. It has the characteristics of Ad-hoc and is difficult to describe uniformly. Therefore, the mainstream data competition detection method is not suitable. Based on the case base of data competition in aerospace embedded software, seven defect models are proposed to describe the harmful interrupt data competition. Aiming at the most common and most difficult to solve the single variable access order pattern, an efficient detection method based on abstract interpretation is proposed to support inter-process analysis and interrupt concurrent analysis. The corresponding detection tool Space DRC is designed and implemented. The experimental results show that Space DRC can detect real data competition in about 21,400 lines of programs in 145ms. Space DRC has been applied in many key spaceflight models, and the efficiency of special analysis for interrupting data competition has been improved by at least five times. It also reduces the problem omission rate.
【作者單位】： 北京控制工程研究所;北京軒宇信息技術(shù)有限公司;中國空間技術(shù)研究院;
【基金】：國家自然科學(xué)基金(91118007)~~
【分類號】：TP311.11

【相似文獻】

相關(guān)期刊論文 前10條

1 劉椿年;一個基于抽象解釋的部分演繹過程[J];軟件學(xué)報;1994年11期

2 王蓁蓁;倪慶劍;張志政;邢漢承;;抽象解釋全總域模型[J];中國科學(xué)技術(shù)大學(xué)學(xué)報;2014年07期

3 錢俊彥;趙嶺忠;蔡國永;;基于完備抽象解釋的性質(zhì)強保留抽象研究[J];計算機學(xué)報;2014年08期

4 姬孟洛;王懷民;李夢君;董威;齊治昌;;一種基于抽象解釋和通用單調(diào)數(shù)據(jù)流框架的值范圍分析方法[J];計算機研究與發(fā)展;2006年11期

5 李夢君;李舟軍;陳火旺;;基于抽象解釋理論的程序驗證技術(shù)[J];軟件學(xué)報;2008年01期

6 王正謙;劉久富;陳哲;;基于抽象解釋和數(shù)值熵的數(shù)值程序分析方法[J];計算機技術(shù)與發(fā)展;2014年04期

7 常碩;趙彬;辛文逵;;抽象解釋技術(shù)在嵌入式軟件測試中的應(yīng)用[J];中國測試技術(shù);2007年06期

8 竇增杰;王震宇;姚偉平;陳楠;余弦;;基于抽象解釋的可執(zhí)行代碼值范圍分析[J];計算機工程;2010年22期

9 姬孟洛;齊治昌;;基于抽象解釋自動導(dǎo)出針對WCET分析的程序流信息的方法[J];計算機工程與科學(xué);2006年12期

10 武書彥;蘇青琴;劉久富;;基于抽象解釋的函數(shù)不變量正確性驗證[J];微電子學(xué)與計算機;2012年10期

相關(guān)會議論文 前1條

1 曾勇軍;王清賢;奚琪;;基于抽象區(qū)間域的數(shù)組邊界檢查技術(shù)[A];計算機研究新進展（2010）——河南省計算機學(xué)會2010年學(xué)術(shù)年會論文集[C];2010年

相關(guān)博士學(xué)位論文 前1條

1 曾穎;基于抽象解釋的軟件保護相關(guān)問題研究[D];解放軍信息工程大學(xué);2011年

相關(guān)碩士學(xué)位論文 前2條

1 侯蘇寧;基于抽象解釋的數(shù)值程序分析技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2009年

2 趙修偉;基于抽象解釋的實時軟件WCET研究[D];大連理工大學(xué);2009年

，

本文編號：2153861