Evaluation of formal methods tools applied to a 6U CubeSat attitude control system

Kerianne H. Gross, Jonathan A. Hoffman, Matthew Clark, Eric D. Swenson, Richard G. Cobb, Michael W. Whalen, Lucas Wagner

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

5 Scopus citations


Exhaustive test of complex and autonomous systems is intractable and cost prohibitive; however, incorporating formal methods analysis throughout the system design process provides a means to identify faults as they are introduced and drastically reduce the overall system development cost. Software errors on fielded spacecraft have resulted in catastrophic faults that could have been prevented had formal methods been applied to the system design. In this research, formal methods, such as model checking and limited theorem proving, are applied to the requirements, architecture, and model development phases of the design process of a reaction wheel attitude control system for a 6U CubeSat. The results show that while feasible, several gaps exist in the capability of formal methods analysis tools. The tools are capable of expressing and analyzing some of the properties of the system, but more work is needed to properly address inherent nonlinearities in complex systems.

Original languageEnglish (US)
Title of host publicationAIAA SPACE 2015 Conference and Exposition
PublisherAmerican Institute of Aeronautics and Astronautics Inc. (AIAA)
ISBN (Print)9781624103346
StatePublished - Jan 1 2015
EventAIAA SPACE Conference and Exposition, 2015 - Pasadena, United States
Duration: Aug 31 2015Sep 2 2015

Publication series

NameAIAA SPACE 2015 Conference and Exposition


ConferenceAIAA SPACE Conference and Exposition, 2015
Country/TerritoryUnited States


Dive into the research topics of 'Evaluation of formal methods tools applied to a 6U CubeSat attitude control system'. Together they form a unique fingerprint.

Cite this