Zachary Luppen

I apply formal methods to various aspects of cube satellite projects, which are becoming very popular with several research communities due to their relatively cheap price, fast turnaround times and easy accessibility to space. I work under the supervision of Dr. Dae-Young Lee and Dr. Kristin-Yvonne Rozier. I study how techniques such as formal specification and runtime monitoring can be used to analyze the health of software systems on cube satellites. A cube satellite, like any typical satellite, tends to be composed of an electrical power system (EPS), an attitude determination and control system (ADCS), a communications system, a flight computer and a payload, among other systems. While cube satellites are cheaper and built faster, they still suffer the same problems as large missions, but without the large teams and resources to troubleshoot them. By applying these techniques, I provide future mission designers with reference specification sets and methodologies that can be used to improve the reliability of their missions. I am currently focused on applying these techniques to cube satellite communications systems. Communications system failures are one of the most common causes of failure in cube satellite missions. These systems are absolutely vital to mission success since communication is essential to downlink data and accomplish research objectives. Study of this issue involves three major components in order to address these failures. These are the creation of a reference set of cube satellite communications fault specifications, the development of a distributed hierarchy of specifications that highlight the system’s complexity, and the design of a configuration using the Realizable Responsive Unobtrusive Unit (R2U2) to demonstrate real-time performance evaluation of a cube satellite communications system.