本文關(guān)鍵詞：基于xMAS模型的SpaceWire信譽(yù)邏輯的形式化驗(yàn)證

  更多相關(guān)文章： xMAS模型 信譽(yù)邏輯 SpaceWire 形式化驗(yàn)證 ACL

【摘要】：空間總線(SpaceWire)協(xié)議是應(yīng)用于航空航天領(lǐng)域的高速通信總線協(xié)議,保證其可靠性至關(guān)重要。但是由于通信系統(tǒng)具有隊列量、分布控制和并發(fā)性等特點(diǎn),傳統(tǒng)仿真模擬的驗(yàn)證方法存在不完備性的問題,采用模型檢測方法對高層次屬性進(jìn)行驗(yàn)證時,通常會出現(xiàn)狀態(tài)爆炸的問題�；趚MAS模型對SpaceWire通信系統(tǒng)中的信譽(yù)邏輯進(jìn)行形式化建模、驗(yàn)證,xMAS模型既保留了底層的結(jié)構(gòu)信息,又可以驗(yàn)證高層次的屬性。對通信系統(tǒng)中信譽(yù)邏輯進(jìn)行抽象進(jìn)而建立了xMAS模型,提取了可發(fā)送性、可接收性和數(shù)據(jù)一致性等3個關(guān)鍵屬性,運(yùn)用定理證明工具ACL2對關(guān)鍵屬性的正確性進(jìn)行了自動驗(yàn)證。該方法為驗(yàn)證指導(dǎo)下的系統(tǒng)設(shè)計提供了有效的參考。
【作者單位】： 首都師范大學(xué)信息工程學(xué)院電子系統(tǒng)可靠性重點(diǎn)實(shí)驗(yàn)室;北京化工大學(xué)信息科學(xué)與技術(shù)學(xué)院;北京航空航天大學(xué)機(jī)械工程及自動化學(xué)院;
【關(guān)鍵詞】： xMAS模型 信譽(yù)邏輯 SpaceWire 形式化驗(yàn)證 ACL
【基金】：國際科技合作計劃(2011DFG13000,2010DFB10930) 國家自然科學(xué)基金項目(61373034,61303014,61379019) 北京市教委科研基地建設(shè)項目(TJSHG201310028014),北京市教委(KM201510028015)資助 北京市屬高等學(xué)校創(chuàng)新團(tuán)隊建設(shè)與教師職業(yè)發(fā)展計劃項目(IDHT20150507)
【分類號】：V443.1;TP393.04
【正文快照】： 1引言SpaceWire協(xié)議是歐空局(ESA)為應(yīng)對復(fù)雜空間任務(wù)而提出的一種高速、全雙工串行總線網(wǎng)絡(luò)協(xié)議。它是基于兩個商用標(biāo)準(zhǔn)IEEE 1355-1995和IEEE 1596.3(LVDS),通過對IEEE 1355可靠性、功耗、抗輻射等方面的改進(jìn)后,使其能更好地滿足航空航天應(yīng)用而提出的一種專門用于空間高速數(shù)

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前2條

1 李德識;陳健;孫濤;;SOC的形式化驗(yàn)證方法[J];武漢大學(xué)學(xué)報(工學(xué)版);2008年06期

2 ;[J];;年期

中國重要會議論文全文數(shù)據(jù)庫 前2條

1 吳鈴鈴;周干民;何偉;高明倫;;IP軟核的形式化驗(yàn)證[A];全國第十五屆計算機(jī)科學(xué)與技術(shù)應(yīng)用學(xué)術(shù)會議論文集[C];2003年

2 郭華;莊雷;;電子商務(wù)協(xié)議的形式化驗(yàn)證方法及FR驗(yàn)證實(shí)例[A];2005年全國理論計算機(jī)科學(xué)學(xué)術(shù)年會論文集[C];2005年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 徐昕;VTOS內(nèi)存管理的設(shè)計實(shí)現(xiàn)及其形式化驗(yàn)證研究[D];南京大學(xué);2014年

2 李小波;龍芯2號功能部件半形式化驗(yàn)證方法的研究與實(shí)現(xiàn)[D];首都師范大學(xué);2006年

3 焦金良;基于多項式模型的高層次形式化驗(yàn)證[D];哈爾濱工程大學(xué);2006年

4 張倩;基于可編程邏輯的硬件平臺的設(shè)計與形式化驗(yàn)證[D];北京交通大學(xué);2009年

5 張金磊;形式化驗(yàn)證技術(shù)在EDA軟件開發(fā)中的應(yīng)用[D];西安電子科技大學(xué);2011年

6 馬小龍;形式化驗(yàn)證在Office安全中的應(yīng)用研究[D];中國人民解放軍信息工程大學(xué);2005年

7 丁廣泓;集成電路形式化驗(yàn)證的FPGA加速技術(shù)研究[D];廣西民族大學(xué);2015年

8 張澤恩;基于GSTE中的符號仿真設(shè)計與實(shí)現(xiàn)[D];電子科技大學(xué);2012年

9 林立;基于高階邏輯系統(tǒng)HOL的數(shù)字硬件形式化驗(yàn)證[D];西安電子科技大學(xué);2005年

10 譚力;基于情態(tài)演算的UML形式化驗(yàn)證與OCL約束自動生成研究[D];華東師范大學(xué);2010年

，

本文編號：885211