Evaluation of Formal Methods Tools Applied to a 6U CubeSat Attitude Control System
Document Type
Conference Proceeding
Publication Date
8-31-2015
Abstract
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.
Source Publication
AIAA SPACE 2015 Conference and Exposition
Recommended Citation
Gross, K. H., Hoffman, J. A., Clark, M., Swenson, E. D., Cobb, R. G., Whalen, M. W., & Wagner, L. (2015, August). Evaluation of Formal Methods Tools Applied to a 6U CubeSat Attitude Control System. AIAA SPACE 2015 Conference and Exposition. https://doi.org/10.2514/6.2015-4529
Comments
Session: Flight Software and Autonomy Technologies
This conference paper is published by AIAA and is available by subscription or purchase at the DOI link below.