《航天多核嵌入式軟體可信驗證與系統原型》是依託大連理工大學,由周寬久擔任項目負責人的面上項目。
基本介紹
- 中文名：航天多核嵌入式軟體可信驗證與系統原型
- 依託單位：大連理工大學
- 項目類別：面上項目
- 項目負責人：周寬久
項目摘要,結題摘要,
項目摘要
嵌入式多核處理器具有較強處理能力，在航天系統得到廣泛套用。多核並發程式訪問共享變數時間和順序的隨機性，導致多核嵌入式軟體測試困難。本項目在前期工作基礎上，並考慮航天軟體評測中心實際需求，擬從四個方面進行研究：1、研究基於多核的嵌入式軟體建模及驗證方法，從模型角度證明嵌入式軟體可信性；2、針對多核程式，分別從靜態代碼分析和動態運行角度研究檢測並發程式原子性侵犯（Atomicity Violation）以及數據競爭（Data Race）行為；為提高測試效率，研究程式執行過程記錄和快速重演方法；3、由於多核Cache命中率以及並發程式運行不確定性，研究採用微觀結構分析和巨觀性能統計預測相結合的多核嵌入式軟體WCET評估方法；4、在前期C/C++原始碼靜態分析基礎上，研究多核並發程式BUG特徵、形式化及匹配算法，檢測並發程式錯誤。最後，開發原型系統對上述方法予以驗證，並在航天軟體評測中心實際套用。
結題摘要
嵌入式多核處理器具有較強處理能力，在航天系統得到廣泛套用。多核並發程式訪問共享變數時間和順序的隨機性，導致多核嵌入式軟體測試困難。本項目在前期工作基礎上，並考慮航天軟體評測中心實際需求，從兩個方面進行研究：1、研究多核嵌入式軟體形式化建模及驗證方法，從模型角度證明嵌入式軟體可信性；2、由於體系結構特性和執行緒調度不確定性，研究了基於時間Petri網的多核嵌入式軟體WCET評估方法，解決多核軟體性能評價問題。
