Formal verification of decision logic for automatic maneuvering of spacecraft∗

Kerianne L. Hobbs, Ivan Perez, Aaron W. Fifarek, Eric M. Feron

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations


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.
Original languageEnglish (US)
Title of host publicationAIAA Scitech 2019 Forum
PublisherAmerican Institute of Aeronautics and Astronautics Inc, AIAA
ISBN (Print)9781624105784
StatePublished - Jan 1 2019
Externally publishedYes


Dive into the research topics of 'Formal verification of decision logic for automatic maneuvering of spacecraft∗'. Together they form a unique fingerprint.

Cite this