AdaCore’s GNAT Ada development environment and Altran Praxis’ SPARK tools are being used at Vermont Technical College during the implementation of two NASA-sponsored programs: continued work on a CubeSat and development of an Arctic Sea Ice Buoy.
Described by AdaCore as being “vastly different applications,” the projects are similar in the sense that "both require extremely high reliability."
The CubeSat autonomous space satellite measures about 100 mm per side. Its maximum mass of 1.33 kg consists of various systems and instruments, including power, attitude determination and control, communications, and other mission-specific payloads, such as a camera to photograph Earth from space. Because such "nano-satellites” are relatively inexpensive, they are being used by a growing number of institutions and countries to collect data for everything from national surveillance to wildlife tracking.
Although the CubeSat is not a safety-critical system, the software for such a system is mission critical. Because of its small size, uploading software patches is not feasible. And, there is no doubt that satellite malfunction due to any type of error, be it mechanical or software, costs time and money that is almost impossible to get back.
In terms of that software component, VTC students have said that Ada offered a number of programming advantages over C. Finding and fixing errors took less time, and error rates for Ada in general were considerably lower than projects programmed in C. Overall, the consensus was that Ada was a language well-suited for high-integrity software, efficient to write, and easy to debug. Use of SPARK further increased the integrity of the code.
The software development process was based around AdaCore’s GNAT Programming Studio (GPS) and GNAT Ada compiler, together with Altran Praxis’ SPARK tools. Compilation with SofCheck’s AdaMagic generated ANSI C code, and cross-compiling with Rowley Associates’ Crossworks produced the MSP430 object code that ran on the target board. The availability of RavenSPARK, the SPARK subset of the Ada Ravenscar Profile (a restricted set of Ada concurrency features suitable for safety-critical systems), allowed students to use SPARK for the real-time, high-integrity programming that is crucial for proper interaction between the CubeSat’s various systems and instrumentation.
VTC is also working on a project for NASA that entails developing the technology that could send a CubeSat to the moon. The premise involves launching a CubeSat from a geo-stationary satellite into lunar orbit. An allied task is to develop a system that would direct that CubeSat down to the moon for a soft landing.
The VTC team will have the task of developing two mini-propulsion systems for the boosters, plus the lunar landing technology. One of the propulsion systems may use a catalyst-ignited mono-propellant mixture of hydroxyl ammonium nitrate and methanol. The second system being contemplated is a photovoltaic-powered ion drive booster with a propellant load of xenon.
Professors and students at the University of Vermont are charged with using mathematical modeling to analyze possible trajectories, radiation exposure, and other parameters. And a team from Norwich University in Vermont will tackle development of the optical systems necessary for space navigation.
This past August, NASA awarded VTC a launch opportunity so a single CubeSat can be launched with a NASA mission in 2012. This CubeSat will contain the GPS/celestial navigation system with NASA Goddard-developed GEONS (GPS Enhanced Onboard Navigation System) software rewritten in Ada/SPARK.
If all goes well, the Vermont project may be awarded the next stage of funding—a $750,000, three-year grant that would allow the team to build the real thing—and send it to the moon.
In collaboration with U of V, VTC is constructing a remote sensing buoy that will be deployed on the Arctic sea ice north of Alaska. The buoy will gather information concerning location, temperature, wind speed, and wind direction. These data values, which will be transmitted back to Vermont using the Iridium satellite network, will be used to refine models of ice movement as it melts. Students are producing the prototype buoy, and a follow-on grant will fund placement of 10 to 20 buoys on the Arctic Ocean ice.
The prototype buoy shares some of the same characteristics as the CubeSat: low power availability, harsh environmental conditions, and the need to be reliable and autonomous.
Since maintenance is not feasible once the buoy is deployed, reliability is paramount. A software crash would devastate the project, and software errors—causing incorrect data to be transmitted—would result in failure of the mission. In addition, the platform is extremely resource-constrained; therefore, the students needed the smallest run-time library possible. The current software uses no run-time library at all for the buoy, but one will probably be needed for the CubeSats.
Software for control of the radio, power management, and telemetry was carried over from the CubeSat software development to the buoy project. Although the buoy software is considerably simpler than that of the CubeSat, it requires the same extreme software reliability. As a result, the combination of Ada, GNAT, and SPARK was used for this project as well. The language and tools provided the necessary reliability and achieved a reduced memory footprint.