Introduction

Welcome to the Flying SPARKs blog!

This is the official blog of the CubeSat development team at Vermont Technical College (VTC). We are a group of students, faculty, and staff who are building spacecraft around the CubeSat standard. Classic "1U" (one unit) CubeSats are only 10 cm on each side and mass limited to 1.33 kg. Yet, thanks the miniaturization of modern electronics, these small spacecraft are still able to perform many useful functions.

There are numerous groups (academic, industrial, and governmental) who are building CubeSat spacecraft. What makes us different than the others is that we are using the SPARK programming language and tool set for our software development.

SPARK is a dialect of Ada that allows for the formal verification of programs. Using the SPARK tools it is possible to mathematically prove that one's software is free of many important classes of errors. Since CubeSat software is difficult or impossible to modify once it is deployed in space, increasing the robustness of that software is of great importance. The recent software problem with the Planetary Society's LightSail spacecraft is an example of the kind of error we hope to avoid by using SPARK.

Any member of the CubeSat development team at VTC can be an author on this blog. It is here where we share our musings about our work and post updates about our progress.

Enjoy!