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

作     者：李艳春 李晓娟 关永 王瑞 张杰 魏洪兴 LI Yan-chun;LI Xiao-juan;GUAN Yong;WANG Rui;ZHANG Jie;WEI Hong-xing

作者机构：首都师范大学信息工程学院电子系统可靠性重点实验室北京100048 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191 

基　　金：国际科技合作计划(2011DFG13000 2010DFB10930) 国家自然科学基金项目(61373034 61303014 61379019) 北京市教委科研基地建设项目(TJSHG201310028014) 北京市教委(KM201510028015)资助 北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507) 

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2016年第43卷第2期

页      码：113-117,134页

摘      要：空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议,保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。

主 题 词：xMAS模型 信誉逻辑 SpaceWire 形式化验证 ACL2 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.11896/j.issn.1002-137X.2016.2.026

馆 藏 号：203767089...