基于xMAS模型的SpaceWire信誉逻辑的形式化验证

发布时间：2017-09-20 02:00

  本文关键词：基于xMAS模型的SpaceWire信誉逻辑的形式化验证

  更多相关文章： xMAS模型 信誉逻辑 SpaceWire 形式化验证 ACL

【摘要】：空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议,保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。
【作者单位】： 首都师范大学信息工程学院电子系统可靠性重点实验室;北京化工大学信息科学与技术学院;北京航空航天大学机械工程及自动化学院;
【关键词】： xMAS模型 信誉逻辑 SpaceWire 形式化验证 ACL
【基金】：国际科技合作计划(2011DFG13000,2010DFB10930) 国家自然科学基金项目(61373034,61303014,61379019) 北京市教委科研基地建设项目(TJSHG201310028014),北京市教委(KM201510028015)资助 北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)
【分类号】：V443.1;TP393.04
【正文快照】： 1引言SpaceWire协议是欧空局(ESA)为应对复杂空间任务而提出的一种高速、全双工串行总线网络协议。它是基于两个商用标准IEEE 1355-1995和IEEE 1596.3(LVDS),通过对IEEE 1355可靠性、功耗、抗辐射等方面的改进后,使其能更好地满足航空航天应用而提出的一种专门用于空间高速数

【相似文献】

中国期刊全文数据库 前2条

1 李德识;陈健;孙涛;;SOC的形式化验证方法[J];武汉大学学报(工学版);2008年06期

2 ;[J];;年期

中国重要会议论文全文数据库 前2条

1 吴铃铃;周干民;何伟;高明伦;;IP软核的形式化验证[A];全国第十五届计算机科学与技术应用学术会议论文集[C];2003年

2 郭华;庄雷;;电子商务协议的形式化验证方法及FR验证实例[A];2005年全国理论计算机科学学术年会论文集[C];2005年

中国硕士学位论文全文数据库 前10条

1 徐昕;VTOS内存管理的设计实现及其形式化验证研究[D];南京大学;2014年

2 李小波;龙芯2号功能部件半形式化验证方法的研究与实现[D];首都师范大学;2006年

3 焦金良;基于多项式模型的高层次形式化验证[D];哈尔滨工程大学;2006年

4 张倩;基于可编程逻辑的硬件平台的设计与形式化验证[D];北京交通大学;2009年

5 张金磊;形式化验证技术在EDA软件开发中的应用[D];西安电子科技大学;2011年

6 马小龙;形式化验证在Office安全中的应用研究[D];中国人民解放军信息工程大学;2005年

7 丁广泓;集成电路形式化验证的FPGA加速技术研究[D];广西民族大学;2015年

8 张泽恩;基于GSTE中的符号仿真设计与实现[D];电子科技大学;2012年

9 林立;基于高阶逻辑系统HOL的数字硬件形式化验证[D];西安电子科技大学;2005年

10 谭力;基于情态演算的UML形式化验证与OCL约束自动生成研究[D];华东师范大学;2010年

，

本文编号：885211