GAP Member Projects

The following are some examples of how Ada is being used in Academic projects by GAP members around the world.

Vermont Technical College

Flight Software for Lunar IceCube Satellite

The Lunar IceCube project is 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.

Bristol University (Bristol, UK)

Verified Robot Control Software

At the University of Bristol and at the Bristol Robotics Laboratory we want to trust our robots. We develop their control software in Ada/SPARK and verify it using the latest technology from AdaCore. Within the RIVERAS project (Robust Integrated Verification of Autonomous Systems) we aim to create systems that behave predictable even in the face of unpredicted events.

HSR University of Applied Sciences Rapperswil Switzerland

The Muen Separation Kernel

Trustworthy by Design -- Correct by Construction Today, even vital infrastructures like power grids, classified government networks or company research sites tend to be connected to the Internet to take advantage of remote management and cloud services. Traditional approaches to securing these infrastructures rely on a strict isolation of critical systems from untrusted networks. In the presence of critical networked environments, other strategies are required to prevent unauthorized access which may be gained through the exploitation of errors in the complex software stacks that are used. One solution are component-based high-assurance platforms where untrusted software components are strictly isolated from security-critical functions on one single physical system.

Vermont Technical College

Lunar CubeSat

Vermont Technical College successfully launched a lunar cube satellite into orbit. The tiny satellite, measuring only 10 cm x 10 cm x 10 cm and weighing 1.1 kg, was launched into a 500 km earth orbit, where it will remain for about three years to test the systems that will be used for the eventual lunar mission. The CubeSat project is part of NASA’s ELaNa IV program (Educational Launch of Nano-satellites).

HSR University of Applied Sciences Rapperswil Switzerland

Trusted Key Manager for IKEv2

IPsec relies on the correct operation of the Internet Key Exchange (IKE) protocol to meet its security goals. The implementation of IKE is a non-trivial task and results in a large and complex code base. This makes it hard to gain a high degree of confidence in the correct operation of the code.

Kansas State University, Manhattan, Kansas (US)

SPARK in Formal Verification Research

Prof. John Hatcliff and his team at Kansas State University’s Static Analysis and Transformation of Software (SAnToS) Laboratory have found the SPARK language technology to be an ideal research vehicle for exploring novel techniques in formal program verification. The SAnToS team has worked for over a decade on innovative tools that incorporate model checking, symbolic execution, data flow, and program dependence analyses. “We started out using Java”, said Prof. Hatcliff. “But Java is a large language with complex semantics, and it certainly wasn’t designed for, or often used in, safety-critical systems. It was hard for us to produce clean technical results and robust tools with Java, and to apply those tools to interesting safety-critical examples. SPARK has proved to be a much more appropriate base language.”

University of Udine

Peer-to-Peer Epi-Transport Protocol

The DSP group at the University of Udine is developing PPETP (Peer-to-Peer Epi-Transport Protocol), a new streaming protocol based on a peer-to-peer approach that will allow to distribute efficiently live multimedia material to a large number of users.  Initially aimed to the specific application of multimedia streaming, the protocol evolved with time and now it can be considered a general-purpose overlay multicast protocol with many features (e.g., efficient use of bandwidth, NAT-traversal built-in procedures, countermeasures against security issues specific to peer-to-peer networks) that make it suitable for efficient multimedia streaming.

The Australian National University

Undergraduate Ada Projects - Gliding in Space

At The Australian National University, students from the 2011 class in Concurrent and Distributed Systems provide an example of the high performance code they developed in undergraduate courses. The aim of the demo is to recharge all vehicles in a variable size swarm at an uncontrollable, roaming fuelling globe in a fully distributed manner. Each vehicle runs its own processes and can only communicate with nearby vehicles. It is a great example showing that GNAT is robust enough to serve as a workhorse in large multi-platform undergraduate class where substantial amounts of code is involved.

United States Air Force Academy

Ironsides Secure DNS Server

Dr. Martin C. Carlisle, the director of the Academy Center for Cyberspace Research at the United States Air Force Academy has developed a secure DNS server using Ada and the SPARK formal methods tool set.

Western Washington University (Bellingham, Washington, US)

Real-Time control of a Model Railway System

At Western Washington University, students are using Ada in senior capstone projects on real-time control of a model railway system. To assist in understanding the complexities of that system, WWU faculty member Martin Osborne has developed a simulator that runs virtual trains on a virtual layout identical to the physical layout in the lab, including all switches and sensors. Use of the simulator during problem analysis has helped students understand the factors to be considered in system specification. In later project stages, the simulator assists in design verification and in more extensive software testing than would be practical with the physical system.

Universidad Politécnica de Madrid (Madrid, Spain)

Real-Time System Development in Ada using LEGO MINDSTORMS NXT

Our purpose at the UPM is to provide a set of tools to fully develop a real-time application in Ada using as target the LEGO® Mindstorms® NXT robotics kit. These tools, working under Linux, provide real-time & embedded systems teachers with an alternative to conventional software models designed in classrooms and labs.

Telecom ParisTech (Paris, France)

Battling Robots: European Robotics Cup

The Telecom Robotics club at Telecom ParisTech (an engineering college in the French Grandes Écoles system) is using Ada and the GNAT technology for its projects.

University of Virginia (USA)

ECHO: A Practical Approach to Formal Verification

At the University of Virginia, Ada lies at the core of a comprehensive approach to creating software for safety-critical applications. Dr. John Knight and his student, Xiang Yin, have created a practical approach to formal verification called Echo. In Echo verification, a program written in SPARK Ada is verified to conform to its SPARK annotations using the SPARK tools.

The Australian National University (Canberra, Australia)

Serafina Autonomous Mini Submersible

At the Australian National University (ANU), Ada plays an integral part in teaching and research, at both the undergraduate and graduate levels. Dr. Uwe Zimmer has been using Ada, with the GNAT technology on Linux, Windows, Mac, and Embedded MPC5554, in two major courses: Concurrent and Distributed Systems, for Computer Science and Engineering students in their second year; and Real-Time and Embedded Systems, for Computer Science and Engineering students in their last year and for Masters students.

Vermont Technical College (USA)

Arctic Sea Ice Buoy and CubeSat Projects

Under the direction of Professors Carl Brandon and Peter Chapin, students at Vermont Technical College are using AdaCore’s GNAT development environment along with Praxis’ SPARK tools on two NASA-sponsored programs with large software components.

Mälardalen University (Västerås, Sweden)

Dasher! – A Racing Robot in Ada

Under the direction of Professor Lars Asplund, graduate students at Mälardalen University are designing, building and programming the Dasher robot in a project that is pushing the limits of robotics technology. The software is being developed with AdaCore’s GNAT toolset, furnished to the university under the GNAT Academic Program (GAP), on Wind River Systems’ VxWorks real-time operating system.