Case Studies

AdaCore has decades of experience providing tools and services to customers for applications with the most demanding software safety, security and reliability requirements. Our collection of case studies demonstrate the effectiveness and real-world application of AdaCore technologies.

Latitude

Latitude Adopts Ada and SPARK for Light Launcher Software in New Space Industry

In the competitive New Space industry, ingenuity, reliability, and cost-effectiveness are paramount factors. When Latitude embarked on creating their cutting-edge small satellite launcher, Zephyr, they recognized the importance of selecting the right programming language and development tools to support their efforts. After evaluating a number of candidates, Latitude settled on Ada and its formally verifiable SPARK subset. Ada and SPARK were judged to have the best support for sound software engineering practice, thus reducing life cycle costs, while meeting real-time embedded systems performance and predictability requirements.

Software Improvements

Software Improvements: Using Ada to Implement a Secure Electronic Voting System

Electronic election systems need to be demonstrably secure in order to ensure the protection of votes, the privacy of voters, and the prevention of interference. That’s why Software Improvements selected the Ada 2012 programming language and AdaCore’s GNAT Pro Ada development environment to upgrade the Australia Capital Territory’s Electronic Voting & Counting System (eVACS®), a public-facing system that demands a high level of security.

NVIDIA

NVIDIA: Adoption of SPARK Ushers in a New Era in Security-Critical Software Development

As one of the world's most trusted names in high-performance computing, security is essential to NVIDIA’s brand. With cybersecurity risks rising across the board, the company took an ambitious path to examine its software development methodology and find a more measurable solution. Ultimately, it chose to abandon C/C++ and adopt SPARK as its coding language of choice for verifying its most security-critical software and firmware components.

ITEC

Ada at ITEC: Real-Time Control over Complex Semiconductor Manufacturing Processes

Semiconductor manufacturing has some of the most exacting needs when it comes to performance and reliability, requiring millisecond-level precision and the ability to cost-effectively produce billions of smaller and smaller devices every year. That’s why ITEC, one of the major semiconductor manufacturing equipment and automation providers, chose Ada as its programming language to develop its critical control software.

IPESOFT

IPESOFT: Delivering reliable, long-lived energy and industrial systems with Ada and AdaCore

When IPESOFT was looking to develop its core real-time D2000 industrial automation platform, it knew that choosing the right development language and software tools would be crucial to the success of the platform and the company’s overall business growth. The solution needed to be reliable, secure, high performance, and easy and efficient to maintain over the long-term. Ultimately, IPESOFT chose AdaCore’s GNAT Pro and the Ada language to develop its D2000 platform.

LASP

Raising the Reliability of Scientific Space Exploration

How Ada is helping the Laboratory for Atmospheric and Space Physics minimize risk, reduce cost, and assure reliable control of software used for spacecraft and instrument operations.

Masten Space Systems

How Masten Space Systems is Using Ada and SPARK to Land on the Moon’s South Pole

To develop their mission-critical flight control software, Masten chose the Ada and SPARK programming languages, together with AdaCore’s GNAT Pro integrated development environment and the SPARK Pro static analysis tool suite for their XL-1 Lunar Lander. The lander will transport a suite of scientific research payloads to the lunar south pole.

SEAKR

How to Develop Reliable Spacecraft Systems at Lower Cost with the Ada Programming Language

When SEAKR Engineering decided to upgrade its mission-critical data recorder applications to a new hardware platform, they kept their software in Ada. To help them improve the efficiency and reliability of their Ada code, they upgraded their development environment to GNAT Pro.

Welch Allyn® devices — a Hillrom product family

Ada and SPARK: Beyond Static Analysis for Medical Devices

The need for safe and secure software — including Medical Device software — is becoming more important as cybersecurity threats in the healthcare sector become more frequent and severe. Hillrom migrated to Ada and SPARK to verify the safety of the code by formally proving some properties, and improving its efficiency by removing dynamic checks, all the while keeping development and verification costs down. Read the full case study to find out more.

BAE Systems Eurofighter Typhoon

BAE Systems Eurofighter Typhoon

BAE Systems are using the GNAT Pro development environment for host Ada compilation in the development of software for the Eurofighter’s mission computers.

MDA - Canadian Space Arm

MDA - Canadian Space Arm

MacDonald Dettwiler (MDA) chose open-source GNAT Ada 95 from Ada Core Technologies to develop control software for the Mobile Servicing System (MSS), an essential com- ponent of the International Space Station (ISS).