Primary funding for this effort is being provided by the Vermont Space Grant Consortium under NASA grant number NNG05GH16H.

A CubeSat is a miniaturised satellite with dimensions of 10x10x10cm which can be doubled or tripled in length. Its combination of size and standardised components make it a much cheaper method of space research than traditional satellites. Consequently it has been rapidly adopted by universities and research institutions around the world for projects covering areas as diverse as earthquake detection and wildlife tracking.

SPARK is a high level programming language and toolset designed to support the development of software where correct operation is vital, for example in safety, security or other “must work” applications. SPARK was adopted for the CubeSat project because of Vermont Technical College's experience in using SPARK and the related Ada programming language in developing mission critical control systems for a project to create Arctic sea ice monitoring buoys. Both the CubeSat and buoy systems face similar challenges in terms of coping with inhospitable conditions and the impossibility of fixing any software bugs when deployed.

The Vermont CubeSat project, led by Professor Carl Brandon of Vermont Technical College aims to launch by 2015. It is developing the first CubeSat that can be launched from a geostationary orbit to successfully land on the moon. The CubeSat electronics are based on a Texas Instruments (TI) MSP430 processor and the software will control navigation, communications, scientific instruments, camera and the CubeSat's propulsion system.

“The scale and simplicity of the CubeSat concept opens up space to innovative projects such as ours,” said Professor Carl Brandon, Professor of Physics, Vermont Technical College. “However the small size of the CubeSat shouldn't mask the ambitious scope of what we are aiming to do.

This means we needed to develop software that met the highest standards of integrity – you simply can't fix software problems in space. SPARK was therefore the perfect choice for this project and is an integral part of our goal to land the first CubeSat on the Moon.”

The proposed lunar lander will be a single unit CubeSat with four mini-thrusters on the bottom to maximise control and manoeuvrability. Two potential options for propulsion are being examined – a bi-propellant booster or a Xenon powered ion drive booster. The Xenon thruster can also be used for a triple CubeSat that would go to and orbit the moon.  The team is currently working on initial designs for the spacecraft, with the aim of achieving further NASA funding in June 2011.

“To succeed scientific research needs to bring together innovation, new ideas and proven technology,” said Keith Williams, Altran Praxis Managing Director. “This new lunar mission demonstrates the potential of the CubeSat concept when combined with advanced, high integrity software developed using SPARK.  We wish the project team well in their ambitious moon mission.”

Developed by Altran Praxis, the SPARK Toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case in line with the requirements of industry regulators and certification schemes.

Visit Altran Praxis at www.altran-praxis.com