Formal verification applied to autonomous spacecraft attitude control

Formal verification tools are cited as an essential component to enable more widespread development and adoption of advanced autonomous systems. While numerous techniques and tools exist, the applicability of these tools to actual systems under development is currently uncertain. There are myriad reasons for such uncertainty, mostly stemming from assumptions necessary for such tools to work, such as: 1) The assumption that an underlying dynamics model or Simulink model is available, 2) The assumption that the dynamics are low-dimensional, 3) The assumption that the dynamics are linear or linearizable without sacrificing accuracy, and 4) The assumption that the underlying controllers and autonomy algorithms are available and easily modeled. This paper first presents a novel satellite benchmark that incorporates autonomous switching between multiple modes of operation related to attitude control. The result is a hybrid system with nonlinear rotational dynamics restricted to a manifold within each mode. Several open source verification tools are then applied to this benchmark to determine any results that can be drawn about the stability of the overall system. We provide a thorough comparison and discussion of the benefits and drawbacks of those tools we tested, none of which were capable of completely verifying stability requirements over the entire benchmark to the best of our efforts. We also discuss the significant hurdles that remain to implementing these tools on realistic autonomous systems, and the techniques we have found to be the most applicable. The contributions of this paper are: 1) a challenging benchmark on which developers can test their verification tools, and 2) a useful starting point to anyone who wants to apply formal methods to autonomous aerospace systems and to advance the conversation on what remains to be accomplished for these tools to be of practical use.