Liverpool (UK) – UK Space Conference, NEW YORK, and PARIS, July 14, 2015 – AdaCore today announced the start of the Lunar IceCube project, 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.”
About AdaCore
Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical, and security-critical systems. Four flagship products highlight the company’s offerings:
- The GNAT Pro development environment for Ada, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability,
- The CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software,
- The SPARK Pro verification environment, a toolset based on formal methods and oriented towards high-assurance systems, and
- The QGen model-based development tool, a qualifiable and customizable code generator and verifier for Simulink® and Stateflow® models, intended for high-integrity control systems.
Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as space systems, commercial avionics, military systems, air traffic management/control, rail systems, medical devices, and financial services. AdaCore has an extensive and growing world-wide customer base; see www.adacore.com/customers/ for further information.
AdaCore products are open source and come with expert on-line support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com
About SPARK
SPARK is a software development technology specifically designed for engineering high-reliability systems. It combines a programming language and a verification toolset to reduce the effort in developing ultra-low defect software in critical applications, for example where safety and/or security are key requirements. SPARK offers verification that is sound and deep and exhibits a remarkably low false-alarm rate. It has a solid industrial track record with a 25+ year history of successful usage worldwide in a range of industrial applications including civil and military avionics, railway signaling, cryptography, and cross-domain solutions.
SPARK 2014 is the next generation of this leading software technology, offering key benefits such as support for hybrid verification (combining formal methods with traditional testing), executable contracts, a larger Ada language subset (for example including generic units), and convergence with Ada 2012 syntax (making it easier to combine Ada and SPARK components). For further information please visit www.spark-2014.org/.
– See more at: http://www.adacore.com/press/spark-going-to-the-moon/#sthash.IondTuYv.dpuf
