Abstract:
As the "nerve center" of spacecraft data/ control, SpaeWire structure and application design of its network layer are important influencing factors of system reliability. In the process of designing and deploying SpaceWire network, in order to analyze it formally, find defects and improve the reliability, a formal analysis template framework for SpaceWire network layer analysis is proposed. All the components of the network layer: real-time packet, terminal node, router and routing mechanism are modeled as timed automata. Then a simplified case is built in the UPPAAL model checking tool, and the extraction property is verified. The analysis of typical cases verifies the effectiveness of the proposed method.