SoylentNews

Arthur T Knackerbracket has found the following story:

My colleague, Carl Brandon, and I have been running the CubeSat Laboratory at Vermont Technical College (VTC) for over ten years. During that time we have worked with nearly two dozen students on building and programming CubeSat nano satellites. CubeSats are small (usually 10cm cube), easily launched spacecraft that can be outfitted with a variety of cameras, sensing instruments, and communications equipment. Many CubeSats are built by university groups like ours using students at various skill levels in the design and production process.

[...] Like all spacecraft CubeSats are difficult to service once they are launched. Because of the limited financial resources available to university groups, and because of on-board resource constraints, CubeSats typically don't support after-launch uploading of software updates. This means the software must be fully functional and fault-free, with no possibility of being updated, at the time of launch

Many university CubeSat missions have failed due to software errors. This is not surprising considering that most flight software is written in C, a language that is difficult to use correctly. To mitigate this problem we use the SPARK dialect of Ada in all of our software work. Using the SPARK tools we work toward proving the software free of runtime error, meaning that no runtime exceptions will occur. However, in general we have not attempted to prove functional correctness properties, relying instead on conventional testing for that level of verification.

[...] In November 2013 we launched a low Earth orbiting CubeSat. The launch vehicle contained 13 other university built CubeSats. Most were never heard from. One worked for a few months. Ours worked for two years until it reentered Earth's atmosphere as planned in November 2015. Although the reasons for the other failures are not always clear, software problems were known to be an issue in at least one of them and probably for many others. We believe the success of our mission, particularly in light of the small size and experience of our student team, is directly attributable to the use of SPARK.

Original Submission