TY - GEN
T1 - Evaluation of formal methods tools applied to a 6U CubeSat attitude control system
AU - Gross, Kerianne H.
AU - Hoffman, Jonathan A.
AU - Clark, Matthew
AU - Swenson, Eric D.
AU - Cobb, Richard G.
AU - Whalen, Michael W.
AU - Wagner, Lucas
PY - 2015/1/1
Y1 - 2015/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84960374865&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84960374865&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84960374865
SN - 9781624103346
T3 - AIAA SPACE 2015 Conference and Exposition
BT - AIAA SPACE 2015 Conference and Exposition
PB - American Institute of Aeronautics and Astronautics Inc. (AIAA)
T2 - AIAA SPACE Conference and Exposition, 2015
Y2 - 31 August 2015 through 2 September 2015
ER -