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

xMAS-based Formal Verification of SpaceWire Credit Logic

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

SpaceWire protocol is a high-speed communication bus protocol applied to aerospace,so it is very important for communication system to ensure the reliability of the design.Due to the presence of a large number of queues,distributed control and concurrency,the traditional verification methods have incomplete defects and state explosion when model checking occurs.This paper presented a formal verification method of credit logic in SpaceWire communication system with xMAS model.xMAS model retains the structural information in lower level and can verify high-level attributes.The paper built an abstract xMAS model for credit logic and listed three key properties including sending,receiving and data consistency.Correctness of the properties was verified automatically by the ACL2 theorem proving tool.It can provide effective reference for system design under the guidance of verification.