Ada Benefits High-Reliability Transportation
An interview with AdaCore’s Greg Gicca shows how Ada aids in the safety, security and software reliability for transportation systems.
[ Editor's note: A couple of corrections to this article need to be noted: 1. AdaCore does sell products and services, such as GNAT Pro that's tested and supported for the host/target pair; 2. Table 1 represents only a partial list of the platforms on which Ada is supported, either by AdaCore or other industry vendors; that is: Table 1 should not be taken as a comprehensive list. We apologize for any confusion.
Chris A. Ciufo, Editor.]
Today, it’s all about using the best software language for the task at hand, be it C/C++, Java or Ada. Certainly anyone working on safety- or security-critical systems should become familiar with Ada, a formerly “niche” military programming language that’s not just for the DoD anymore. The benefits Ada brings are enormous in applications that cannot be allowed to fail and rely on robust software in medical, industrial, avionic, industrial, and transportation market segments.
In fact, all of these markets have similar safety (and increasingly “security”) requirements. In transportation alone, the tens of millions of daily passengers on railways, subways, roadways and in the air all expect to arrive at their destination safely and on time. They don’t think about source lines of code, priority inversions or software bugs, and they don’t expect hackers to compromise a city’s traffic signals like in the movie The Italian Job. Ada is an ideal language upon which to build secure, reliable software for safety-critical transportation systems.
We recently caught up with Greg Gicca, director of safety and security at AdaCore, and discussed how Ada fits into transportation applications. AdaCore is a recognized worldwide expert on the Ada language. Founded in 1994 with offices in New York and Paris, the company is stuffed with computer scientists and bona fide Ada language gurus. What follows are edited excerpts from that discussion, along with case studies available from AdaCore and their end users in industries related to transportation, air traffic control, and aviation.
But…What is Ada?
Ada was developed by a working group sponsored by the US Department of Defense (DoD) in an effort to consolidate the number of high-level software languages used in military projects. According to Wikipedia, Ada helped reduce the number of languages from 450 to 37 between 1983 and 1996. Ada is still a requirement on many new DoD programs and it continues forward migration (with backwards compatibility) as proven legacy code gets reused on recapitalized DoD systems. But the DoD might be considered an anomaly, having the ability to create technology from scratch and mandate its use. So Ada might be considered some sort of a “one-off,” used only by the military. That’s not true since Ada has many features that makes it ideal for safety- and security-critical systems.
Ada is a simple language that uses readable syntax such as “+” for addition and plain language conditions such as “if…end.” This makes it easier for humans to debug since the symbols used in other languages don’t come naturally and may be easily missed by developers. Ada doesn’t allow buffer overflows, a common mechanism used by hackers to corrupt a system and cause it to go unstable. Ada is also structured, object oriented, and strongly typed. This latter is one of Ada’s most redeeming features since it means there’s not a lot of ambiguity on how code is written. Wikipedia points out that Ada’s strong typed restrictions include:
- absence of unchecked run-time errors
- strong guarantees about run-time behaviors
- type safety that rejects function calls that disregard data types
- well-defined errors
- myriad other locked-down constructs that force the programmer to follow Ada’s rules which disallow room for interpretation.
Transportation systems, like Switzerland’s many high-speed railways, absolutely depend on software that has strongly typed features (Figure 1). It should be comforting then that railway control systems manufactured by Siemens Mobility use GNAT Pro, a version of the Ada language with a tool suite from AdaCore. “Safety has the highest priority in the railway business,” says Daniel Bigelow, Siemens software developer. “We invest a lot of time and energy in code-review and testing activities. [One of] our two most important requirements [was] an Ada compiler that could be configured to analyze code against a rigorous set of specific criteria.” Translation: Ada was chosen for Siemens’ safety-critical systems.
|Figure 1: Train control systems rely on safety-critical software that must never fail. Siemens Mobility has selected Ada for the next generation of its railway control and information system. (Courtesy: Siemens Mobility; www.mobility.siemens.com).|
The Siemens railway control system is a modern networked application that covers every aspect of the railway control domain. It uses a distributed architecture to allow a computer to automatically take over control of a cell from another computer in the same cell due to a hardware failure or planned maintenance. This architecture guarantees high-availability of the system in accordance with European railway software standards. The current version of the system controls the train traffic throughout major parts of Switzerland and also parts of Austria, Hungary and Malaysia. Other Siemens railway computer systems are certainly candidates for Ada’s mission-critical assurance, such as the ZSI 127 Intermittent Automatic Train Control System shown in Figure 2. This transportation system monitors train movement using dynamic brake curve computation and applies the brakes in stages. According to Siemens, “data is transmitted on an intermittent basis via RF track-mounted Eurobalises, and also semi-continuously via Euroloop if necessary.” Railway signal controllers, track switchers, and even whole-system traffic monitoring are further examples of places where Ada could be deployed.
AdaCore’s Gicca says that his company’s GNAT Pro Ada compiler and other tools were used to discover problems at the source code level instead of in the lab. Tools developed for Ada by his company essentially automate the code-review process.
What Makes Ada Unique?
Although AdaCore didn’t invent Ada, they did invent GNAT, the GNU Compiler Collection (GCC) eventually made available by the Free Software Foundation for Ada. Since GNAT is obviously available free-of-charge, AdaCore makes its money selling GNAT Pro – the compiler along with some “60-odd tools that go along with Ada”– plus support services via subscription. Technically the company doesn’t sell products; rather, it’s the support for those products. And customers can switch to the fully functional and well-supported free tools at any time. This model allows AdaCore to get deeply involved with its paying customers, which is why, says Gicca, the company has so much domain knowledge on transportation applications such as the unique Siemens system.
|Figure 2: Siemens’ ZSI 127 Intermittent Automatic Train Control System. While it’s unknown if this system uses Ada to automatically control braking, it’s definitely a candidate for Ada’s safety-critical coding practices. (Courtesy: Siemens Mobility; www.mobility.siemens.com).|
Ada itself is also unique for many reasons, not the least of which is the number of platforms on which it can be hosted. A partial list of these platforms – native CPUs, operating systems, real-time operating systems, and cross platforms – is shown in Table 1. This is important in transportation due to the sheer number of different types of systems that make up “transportation”: from railways and subways, to buses, shipping, roadways and more. Each of these platforms uses different computers and infrastructure, and each has a combination of legacy hardware and software but must operate in different regulatory environments which vary by country. And don’t forget, all of these systems have some level of safety, security or both since lives are at stake when the system operates.
Table 1 shows that there are sources to the builds for Windows, Linux, Windows and anything else one could need. Ada was also designed for the types of embedded systems found in many transportation applications and it runs on all of the favorite embedded targets found there. Some of the most popular build platforms for embedded transportation targets include “various flavors of VxWorks, VxWorks-Cert, Vxworks-653, VxWorks for MILS [all available from Wind River], LynxOS [from LynuxWorks], PikeOS from Sysgo and a variety of different embedded platforms.”
One example of a legacy platform that adopted Ada is the FAA’s User Request Evaluation Tool (URET), a conflict-resolution and detection tool for U.S. air traffic controllers. Created by federally funded research lab Mitre’s Center for Advanced Aviation Systems Development, URET helps enable the FAA’s Free Flight program by aiding controllers in meeting pilots’ requests for in-route flight changes due to weather, direct routing requests, or altitude changes for smoother flight or to capitalize on prevailing winds. Without the system, controllers in Air Route Traffic Control Centers (ARTCCs) were forced to rely on paper flight documents, hand calculations and mental notes to decide on granting a pilot’s request while assuring conflict-free route assignment. More automation reduces an element of human error.
|Table 1: A partial list of the platforms that currently support Ada. (Courtesy: AdaCore).|
URET was built by Lockheed-Martin, which used SPARC-based Sun workstations running POSIX thread libraries on Solaris to protect against software priority inversions. Ada was selected as the preferred language for this safety-critical system. Additionally, Lockheed-Martin had proven as reliable some legacy code on different platforms and AdaCore created a “type dictionary support tool” to port between platforms. More specifically, the company used an ASIS-for-GNAT tool based upon the ISO/IEC 15291:1995 international Ada Semantic Interface Specification. Ada was the ideal language to meet the priority inversion avoidance concern as certain POSIX thread priorities were maintained in the Ada program implementation. According to AdaCore, URET was installed at all 20 ARTCCs and is currently helping pilots map shorter routes, safely.
When Ada is Not Enough
For all the goodness of Ada, there are many applications that require more robustness, determinism and security. For those reasons, the SPARK language was created. According to Wikipedia: “SPARK is a formally-defined computer programming language based on the Ada programming language, intended to be secure and to support the development of high integrity software used in applications and systems where predictable and highly reliable operation is essential for reasons of safety.” Examples include avionics, such as those systems with DO-178B safety-critical certifications required; medical systems that mandate FDA certification; process control software in nuclear power plants with U.S. NRC certification; or even air traffic control.
In order to make it deterministic, changes were done such as removing the ability to perform exception propagation and handling. Also removed was general task rendezvous, while contracts were added that assured that certain certifiable requirements in the code were met. This allows programmers and certifying agencies to formally prove the correctness of code by setting, verifying and certifying to requirements. AdaCore notes that for safety and DO-178B, one still has to test the code – you can’t just prove correctness – but one can perhaps test less. (In the latest revision of DO-178C you do get certification credit using SPARK and can test in fact less.) SPARK is also ideal at implementing the Common Criteria certification assurance levels for secure software in EAL levels 1-7 (7 being the highest).
Figure 3: NATS builds the iFACTS system for the UK’s air traffic controllers which uses Altran-Praxis SPARK and tools from AdaCore. (Image courtesy of NATS; http://media.nats.co.uk/).
Says AdaCore’s Gicca, “SPARK now is an open source language that was developed by Altran-Praxis fifteen years ago. AdaCore enhanced the language and added a toolset,” similar to how the company rounded out GNAT Pro. SPARK is a subset of Ada with extensions, which is really unique since most compilers can’t handle a subset and extensions, but as a subset SPARK allows verifiable and deterministic coding like Ada. AdaCore’s partnership with Altran-Praxis was formalized three years ago, and it’s not surprising that Praxis selected GNAT Pro for yet another safety-critical application in air traffic control.
Besides creating SPARK, Altran-Praxis is a UK-based embedded and safety-critical systems integrator, and the company selected GNAT Pro for the UK’s next-generation Interim Future Area Control Tools Support (iFACTS) air traffic control system for its client NATS. According to AdaCore’s Gicca: “iFACTS will use a new program that is being designed and implemented from the start with the SPARK Ada language. The program used the GNAT Pro native toolset on IBM AIX workstations as the development environment.”
iFACTS helps Britain’s air traffic controllers based out of London Area Control Centre, Swanwick to meet increased air traffic and alerts them to flights that deviate from flight plans, something keenly learned in America post-9/11. Lead integrator NATS pioneered research, development and simulation of advanced air traffic control tools prior to contract award in 2007 (Figure 3). Using Ada derivative SPARK, NATS just reported that “figures for February to April 2012 show the average NATS air traffic control (ATC) delay was down to 1.4 seconds per flight compared to an average delay of 132.1 seconds 10 years ago; this is the lowest figure since records began in the mid-1990s.” Clearly the system works, and Ada with SPARK helps to make the software robust and safe.
Chris A. Ciufo is senior editor for embedded content at Extension Media, which includes the EECatalog print and digital publications and website, Embedded Intel® Solutions, and other related blogs and embedded channels. He has 29 years of embedded technology experience split between the semiconductor industry (AMD, Sharp Microelectronics) and the defense industry (VISTA Controls and Dy4 Systems), and in content creation. He co-founded and ran COTS Journal, created and ran Military Embedded Systems, and most recently oversaw the Embedded franchise at UBM Electronics. He’s considered the foremost expert on critically applying COTS to the military and aerospace industries, and is a sought-after speaker at tech conferences. He has degrees in electrical engineering, and in materials science, emphasizing solid state physics. He can be reached at firstname.lastname@example.org.