Academic Courses and Projects
University of Virginia (USA)
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 developer then uses automated Echo tools to simplify the annotated code and extract a specification in the PVS language (PVS is a specification and verification system from SRI). Finally, the extracted specification is shown to refine an original formal specification using the semi-automated PVS proof system.
Echo’s strategy of splitting the formal verification process down the middle and attacking it from both sides dramatically reduces the effort needed to complete a formal verification, enabling Dr. Knight and his students to complete verification of systems as large as 10,000 lines of Ada code. One project that has benefited from Ada and Echo verification is the University of Virginia’s LifeFlow artificial heart pump. Designed for the long-term (10–20 year) treatment of heart failure, this pump has a continuous-flow, axial design. The use of magnetic bearings and computational fluid dynamics simulations permit a streamlined path for blood flow. Compared with earlier pumps that used mechanical bearings, this flow path reduces the damage done to blood cells, thus reducing the potential for the formation of dangerous blood clots.
Control of the magnetic bearings is provided by a Freescale MPC5554 microcontroller executing control software written in SPARK Ada by Patrick Graydon and compiled using AdaCore’s GNAT Pro High-Integrity Edition compiler. The control software runs natively on the microcontroller with no operating system, limiting the software base that must be verified for this safety-critical application. Comprehensive Echo formal verification complements functional testing to Modified Condition / Decision Coverage (MC/DC), providing high confidence that the magnetic bearing controller is as free of defects as can practically be achieved.
For further information about the Echo approach and the LifeFlow project, please see dependability.cs.virginia.edu/info/Echo and dirac.mae.virginia.edu./lifeflow/.
The Australian National University (Canberra, Australia)
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:
4Concurrent and Distributed Systems, for Computer Science and Engineering students in their second year (cs.anu.edu.au/student/comp4330/), and 4Real-Time and Embedded Systems, for Computer Science and Engineering students in their last year and for Masters students (cs.anu.edu.au/student/comp2310/).
Dr. Zimmer selected Ada because of its strong support for sound software development in general, its collection of features for tasking, real-time, and embedded systems in particular, and the availability of the GNAT Ada development environment for the target platforms used in the courses. “In retrospect, Ada was a natural choice, and students are quick to take advantage of the language’s benefits,” said Dr. Zimmer. “Since Ada is standardized and interplatform compatible, many students develop their projects on their own computers and then submit their work without our being able to tell which platform was used.”
Ada-based projects at the ANU include communication systems and sonar processing, and one student will be using Ada (and GNAT for the MPC5554 and AVR processors) for his Ph.D. thesis work on high-integrity design and programming for small Unmanned Aerial Vehicles, specifically helicopters. As summed up by Dr. Zimmer, “We are happy Ada and GNAT users here at the ANU. Ada is a highly efficient teaching tool that leads seamlessly into full industrial deployment, and AdaCore’s support is unparallelled.”
Vermont Technical College (Randolph Center, Vermont, US)
Students Using SPARK and GNAT for Arctic Sea Ice Buoy and CubeSat ProjectsUnder 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. For the first project, the students are designing and building both the hardware and software for an Arctic Sea Ice Buoy that measures wind speed, direction, temperature and GPS position. Data from the buoy are sent back to the home base via the Iridium satellite network. The students are producing the prototype buoy for the study of sea/ice interaction in the Arctic Ocean, and a follow-on grant will fund placement of between 10 and 20 buoys on the Arctic Ocean ice.
The second project is a continuation of work on CubeSat, a space satellite 10 cm in diameter with a mass of 1 kg. The CubeSat software is considerably more complex than that of the Sea Ice Buoy, but the two projects share a common software methodology and some of the code.
“Vermont Tech was one of the first colleges to sign up for the GNAT Academic Program, and we are pleased that AdaCore has taken the initiative in promoting the use of Ada in undergraduate curricula,” said Prof. Brandon. “The ocean and space projects require extremely high reliability: a bug in the deployed software is expensive to fix and may even cause damage to or loss of the equipment. Using the SPARK language with the GNAT compiler and tools has been an excellent experience for the students in how to build high-assurance software.”
A paper by Professor Brandon, describing the software methodology used in the two projects, appeared in the September 2008 issue of Ada Users Journal.
Mälardalen University (Västerås, Sweden)
Run, Dasher, Run! Swedish Students Implement 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.
The Dasher project’s goal is to develop a humanoid (two-legged) robot that can run 100 meters in 9.5 seconds, which would break the human record. Among the many challenges are how to model the physics of sprinting, and how to manage the tradeoff between speed and stability so that the robot does not topple over or move into the lanes of other runners. Since safety is an important factor for robotics, Ada was selected as the implementation language, with concurrency usage adhering to the Ravenscar tasking profile. The project has adopted the Uppaal tool environment for modeling, validating and verifying the robotics software’s real-time properties.
“We are very pleased with the progress on Dasher,” said Professor Asplund. “Thanks to both the Ada language and the GNAT environment, the students have been highly productive and have learned a great deal about robotics, team software projects, and safety-critical system development. That was our goal, and we plan to continue with Ada and the GNAT tools on future projects.” For more information on Dasher, please see www.dasher.se.
Tell us about your project
Do you have an Ada-driven academic project that you’d like to share with us? If so please contact us at: contact@ara.org
