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 (former director of the Academy Center for Cyberspace Research at the USAF Academy, and now at Carnegie Mellon University) and Dr. Barry Fagin (US Air Force Academy) have developed a secure DNS server using Ada and the SPARK formal methods tool set. IRONSIDES is an authoritative DNS server that is provably invulnerable to many of the problems that plague other servers. It achieves this property through the use of formal methods in its design, in particular the language Ada and the SPARK formal methods tool set. Code validated in this way is provably exception-free, contains no data flow errors, and terminates only in the ways that its programmers explicitly say that it can. These are very desirable properties from a computer security perspective.
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.