Flight Software for Lunar IceCube Satellite

Vermont Technical College

The Lunar IceCube project is a major hardware/software development effort that will use the GNAT Pro and SPARK language toolsets to help achieve the high reliability required for space missions. Sponsored by NASA through their NextSTEP initiative (“Next Space Technologies for Exploration Partnerships”), Vermont Tech’s flight software development is part of a lunar exploration program that is being administered by Morehead State University. Lunar IceCube is a follow-on to an earlier NASA-sponsored Vermont Tech project, also developed using GNAT Pro and SPARK, that has been successfully transmitting data from an earth-orbiting CubeSat since its launch in November 2013.

Lunar IceCube is a 6-Unit CubeSat mission to prospect for water and other lunar volatiles in all forms (solid, liquid, and vapor) from a highly elliptical orbit with a low point of 100 kilometers (60 miles) where the data will be gathered, and a high point of 5,000 kilometers (3,100 miles). It will investigate the distribution of these compounds as a function of time of day, latitude, and lunar surface composition. By analyzing the data thus produced, scientists will better understand the underlying processes that shaped the distribution, abundance, origin and evolution of volatiles on the moon. The Lunar IceCube CubeSat will get a free ride to the moon on NASA’s Space Launch System EM-1/Orion test flight in late 2018.

Morehead State will assemble the IceCube hardware including the infrared spectrometer from NASA Goddard Space Flight Center and the Iris data and navigation radio from NASA’s Jet Propulsion Lab. Vermont Tech will develop the flight software that will control all aspects of the CubeSat: the navigation data Iris radio, the BIRCHES infrared spectrometer for chemical analysis of the volatiles, the iodine ion engine, and the attitude determination and control unit.  The software will be implemented in SPARK/Ada using AdaCore’s GNAT Programming Studio (GPS) IDE, GNAT Pro compiler, and SPARK toolset to prove the absence of run-time errors. The IceCube software will be developed by a team of undergraduate students under the direction of Dr. Peter Chapin, with the overall software project managed by Dr. Carl Brandon.

“I chose to use SPARK/Ada for the Lunar IceCube,” said Dr. Brandon, “based on our very positive experience with the language and AdaCore’s tools on our previous CubeSat project. I have been involved with Ada since its beginning and understand the benefits of the technology and the added advantages of the SPARK formal methods approach. So I settled on SPARK/Ada for our earlier project, the Vermont Lunar CubeSat. It was the first CubeSat programmed in Ada, and the first spacecraft of any kind to use SPARK. The software was written by a couple of Vermont Tech undergraduate students with no previous experience with Ada or SPARK. Our CubeSat was launched on November 19, 2013 along with 11 other university CubeSats, two NASA CubeSats, and 14 Air Force CubeSats.  The Vermont CubeSat is the only university CubeSat still operating: eight were never heard from, one fried its batteries the first day (software error), one worked a little for less than a week, and one for four months. I am convinced that our use of SPARK was essential to our CubeSat’s successful accomplishment of its mission. The IceCube software is much more complex, and SPARK is needed more than ever.”

“We have been seeing a surge of interest in SPARK recently from the Space domain,” said AdaCore President Cyrille Comar. “Has Vermont Tech's CubeSat success played a role in this interest? Certainly, but there are other factors. Perhaps this segment of this industry is the first to discover that the new version of SPARK not only goes further in combining static and dynamic verification, but also makes it fairly easy and pleasant to do so. We congratulate Dr. Brandon and his team in pioneering this new way of developing high integrity applications.”