本文關(guān)鍵詞：MPSoC核協(xié)調(diào)可靠性和性能的形式化驗證

  更多相關(guān)文章： 片上多核處理器 核協(xié)調(diào) 混雜變遷系統(tǒng) 混雜馬爾科夫決策過程 隨機時序邏輯 PRISM模型檢測器 數(shù)據(jù)脫敏

【摘要】：為了在早期發(fā)現(xiàn)片上多核處理器(MPSoC)設(shè)計缺陷,提出一種對核協(xié)調(diào)進行結(jié)構(gòu)建模和性質(zhì)刻畫的形式化方法。在標記變遷系統(tǒng)中引入多項式函數(shù)替代動作表達核協(xié)調(diào)過程中對數(shù)據(jù)的改變,加入物理元器件發(fā)生故障的概率屬性,形成用以描述核協(xié)調(diào)可靠性和性能的混雜馬爾科夫決策過程模型。采用隨機時序邏輯刻畫系統(tǒng)性質(zhì),通過模型檢測工具驗證分析,以銀行數(shù)據(jù)脫敏MPSoC為例,分析系統(tǒng)可靠性和時間延遲與能耗等性能指標。這些驗證結(jié)果對于早期MPSoC設(shè)計人員具有較強的指導(dǎo)作用。
【作者單位】： 中國科學(xué)院成都計算機應(yīng)用研究所;中國科學(xué)院大學(xué);貴州銀行博士后科研工作站;廣西民族大學(xué)廣西混雜計算與集成電路設(shè)計分析重點實驗室;
【關(guān)鍵詞】： 片上多核處理器 核協(xié)調(diào) 混雜變遷系統(tǒng) 混雜馬爾科夫決策過程 隨機時序邏輯 PRISM模型檢測器 數(shù)據(jù)脫敏
【基金】：國家自然科學(xué)基金資助項目(11371003;11461006) 廣西科技基金項目(10169-1) 廣西自然科學(xué)基金項目(2012GXNSFGA060003) 廣西教育廳科研項目(201012MS274)
【分類號】：TP332
【正文快照】： 網(wǎng)絡(luò)通信、多媒體、信號處理、科學(xué)計算和信息安全等的蓬勃發(fā)展,使得基于數(shù)據(jù)運算的單一功能環(huán)境,轉(zhuǎn)向基于操作的多任務(wù)、多功能和多制式化環(huán)境發(fā)展[1]。受時鐘、功耗和尺寸等因素的制約,基于單任務(wù)的單核處理器集成已很難滿足新型復(fù)雜應(yīng)用的計算需求。MPSo C使用復(fù)雜的片上網(wǎng)，

本文編號：867665