Formal verification of decision logic for automatic maneuvering of spacecraft∗

As the complexity and number of space operations in Earth orbit continues to grow, there are increased opportunities to incorporate automatic or autonomous maneuvering as part of a space traffic management framework. Understanding the context of the automatic maneuver, including the conditions under which an automatic maneuver is acceptable, is important to the design of the overall automatic maneuver system. This work proposes and conducts formal verification of high-level system requirements to govern automatic maneuvering of satellites in the presence of safety interlocks or failures. Three examples of automatic maneuver contexts are considered: conjunction avoidance, especially in the presence of orbital debris; rendezvous and proximity operations, especially for service satellites and active debris removal; and station keeping, especially in large satellite constellations providing space-based services like Internet. The primary contribution of this paper is the development and analysis of formal requirements for high-level system states governing when an automatic maneuver is acceptable. The requirements serve as a baseline framework for future automatic spacecraft maneuver research.