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

摘要：

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

关键词：xMAS模型、信誉逻辑、SpaceWire、形式化验证、ACL2

所属期刊栏目：43

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2016-05-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：113-117,134