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

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

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

【相似文獻】

中國期刊全文數據庫 前2條

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

2 ;[J];;年期

中國重要會議論文全文數據庫 前2條

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

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

中國碩士學位論文全文數據庫 前10條

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

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

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

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

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

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

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

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

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

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

，

本文編號：885211