When Masten Space Systems was awarded a NASA contract to land scientific payloads on the Moon, the company chose to work with AdaCore’s software development and verification tools for its XL-1 Lunar Lander spacecraft. Masten Space Systems will use the Ada and SPARK programming languages and AdaCore’s GNAT Pro integrated development environment and SPARK Pro static analysis verification tools in the exciting exploration project
Masten Space Systems was awarded the $75.9 million contract by NASA to transport scientific research payloads to the lunar South Pole in April 2020. The NASA Commercial Lunar Payload Services (CLPS) project contract encompasses everything from initial lab work to transportation to the Moon’s surface and a landing to take place in late 2023. There will also be a host of post-landing payload services. The terrain at the lunar South Pole is of huge geological interest, but also very uneven, making it difficult to land a spacecraft and explore with a rover. Once it is in orbit, the Masten lander must navigate the polar region, determine where to land and navigate several potential hazards – all autonomously.
Masten’s XL-1 Lunar Lander boasts numerous small embedded computers called electronic control units (ECUs) that turn the power on and off to various components, control the engines and thrusters, and interface with sensors. Developing the software for these small, heavily constrained ECUs presents a number of challenges. The software will run in a “bare metal” configuration, and it has to be extremely reliable and easy to maintain. The code also needs to be modular and reusable, to avoid duplication of effort and to reduce development costs and timeline.
“We are thrilled to see the Ada and SPARK programming languages being adopted by one of today’s most exciting lunar spacecraft projects,” says Quentin Ochem, Lead of Business Development at AdaCore. “We look forward to helping Masten address the mission’s unique reliability challenges with the novel approach of formally proven software development” Abhimanyu Ghosh, Avionic Software Engineer at Masten Space Systems added: “Masten already sees substantial value in the capabilities that Ada, SPARK, and AdaCore’s products and support have brought to their embedded project. We expect to realise a reduction of at least 20 to 30 percent in verification and validation time and in overall development costs and timelines, as well as a 20 to 30 percent increase in code reuse.”
SPARK is a language plus a toolset. The SPARK language is a formally analysable subset of Ada – a modern programming language used worldwide for the development of critical software. The SPARK toolset brings mathematics-based confidence to software verification through the use of formal methods. GNAT Pro is AdaCore’s comprehensive development environment for producing software systems where efficiency, reliability and maintainability are essential. It comprises a suite of tools and libraries for large, mission-critical applications.
While the XL-1 Lunar Lander project is still in development, Masten already sees substantial value in the capabilities that Ada, SPARK, and AdaCore’s products and support have brought to their embedded project.
