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

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

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

【相似文獻】

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

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

2 ;[J];;年期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：885211