Vermont Technical College
Vermont Technical College successfully launched a lunar cube satellite into orbit. The tiny satellite, measuring only 10 cm x 10 cm x 10 cm and weighing 1.1 kg, was launched into a 500 km earth orbit, where it will remain for about three years to test the systems that will be used for the eventual lunar mission. The CubeSat project is part of NASA’s ELaNa IV program (Educational Launch of Nano-satellites).
The CubeSat’s navigation and control software was developed in SPARK/Ada using AdaCore’s GNAT Programming Studio (GPS) IDE and GNAT Pro compiler and exploiting Altran’s SPARK toolset to prove the absence of run-time errors. The software was developed at Vermont Technical College by a team of undergraduate students under the direction of Dr. Peter Chapin. Although they had no previous knowledge of SPARK or Ada, the students came up to speed quickly and were able to take advantage of SPARK’s various annotations to produce robust code.
“We specifically chose to write the control program for our CubeSat in SPARK because it offers increased reliability over the C language software used in almost all CubeSats to date,” said Prof. Carl Brandon, the project leader from Vermont Technical College. “The success of the fairly complicated software on this ELaNa CubeSat gives us confidence in using SPARK 2014 for the much more complicated and expensive lunar mission.”
“We are delighted to see our technologies once again being launched into space,” said Robert Dewar, AdaCore President. “You only get one shot for this kind of application, so it is critical to produce safe and totally reliable software. In this case, it is very encouraging to see students without prior experience using SPARK and GNAT Pro together to achieve this goal.”
For more information, please visit http://www.cubesatlab.org