Aerospace and defense applications continue to rely on the Ada programming language and SPARK subset as systems – both new innovations and upgraded legacy or traditional solutions – grow in complexity and concerns loom over safety and security. Software engineers worldwide are choosing Ada for a growing number of applications across aerospace and defense and myriad other safety-critical markets, including autonomous vehicles such as driverless cars.
AdaCore Commercial Director Jamie Ayre sat down with Intelligent Aerospace Editor Courtney E. Howard to discuss software development and verification workflows, concerns, challenges, and solutions; autonomous vehicle accidents; recent software engineering trends; and the path to safe, secure, high-integrity and error-free code.
What should companies consider when selecting a language, and software development and verification tools? Any advice you can offer software engineers and managers?
All our customers building critical systems will consider the costs relating to the whole life cycle of the project including development, testing, and especially maintenance. All projects have time constraints but the cost of finding and fixing bugs once the application is deployed is very, very expensive. Ada and SPARK offer an attractive, cost-effective balance between software reliability and time to deployment since they catch errors early, when they are least expensive to correct.
Why is the choice of programming language and software development/verification tools important…
a) for aerospace and defense projects?
Through the choice of programming language and tools, program managers can significantly improve the quality of the software in the deployed application, ease the job of the developer writing the code, and reduce the cost of implementation and certification, should this be required.
Programming languages can provide generic features and built-in checks to help build safety-critical software. Ada is one such language and has a long history of being used in avionics projects. An example of one such feature is contract-based programming, introduced in Ada 2012. Through contracts the developer can formalize the intended behavior of the application, and can verify this behavior by testing, static analysis, or formal proof. Very useful when building critical systems.
The language will only go so far, however, and to help write critical code you need accompanying compilers and tools. At AdaCore, these are available with long-term support, certifiable run-time libraries, and source-to-object traceability analyses (as required for DO-178C / ED-12C Level A). Supplementing the compilers are a comprehensive set of tools, including coding standard checkers, test and coverage analyzers, and static analysis tools.
In the SPARK formal methods-based technology, developers can guarantee a wide range of software integrity properties, such as freedom from run-time errors, enforcement of safety properties or security policies, and full functional correctness. It really is difficult to write better code!
b) particularly for safety-critical systems?
Through safety standards such as DO-178C, EN-50128, etc., certification authorities require developers of safety-critical systems to provide evidence that the software will act in a certain way when required and just as importantly, won’t act in unintended ways. As described above, the choice of programming language and accompanying tools is vital to help with this effort. We have published a couple of booklets that describe in detail how Ada, SPARK, and the GNAT Pro toolset can help for DO‑178C / ED‑12C, for CENELEC EN 50128:2011, and for the Adoption of SPARK (co-authored with Thales).
From its inception, Ada was designed with reliability in mind and over the years users have built thousands of safety-critical systems.
More and more industries are wanting to build applications offering ambitious user features and as such the software used to drive them is becoming more and more complex. At AdaCore, we are seeing Ada’s benefits attracting customers from outside of our traditional aerospace and defense markets.
c) and especially for autonomous systems?
For builders of autonomous systems, the choice of programming language and tools is equally important, and in certain cases more so, as there is no human to “take over the controls.” These systems for the large part will work in public spaces, be it in the air or on the ground. Unexpected behavior, collisions, and overall failure could lead to life-threatening situations.
The reliability of the software is paramount as software drives the autonomy and ensures that the situations described in the previous sentence do not happen. Many autonomous systems will be required to provide the same assurance that their manned, certified cousins do, not least to reassure the public who will interact with them!
Another ever-so-important requirement that the programming language and its supporting development and verification tools can help address is security. It is not sufficient for systems to be “safe,” they also need to be “secure.” AdaCore Technologies for Cyber Security describes how the Ada and SPARK languages and accompanying tools can help develop and verify correct and secure software. As a specific example, we identify how to address the weaknesses identified in the MITRE Corporation’s Common Weakness Enumeration (CWE).
How are Ada and AdaCore solutions being used today?
I invite you to visit our industry page where you will find information around cutting-edge A&D applications. Outside of that market, I would like to highlight one project where we are continuing to work with the automotive industry in their quest to build safer, more secure software. We have recently successfully completed research for DENSO (working with the University of Nagasaki) to show how applying Formal Methods help achieve Freedom from Interference. The ultimate goal is to simplify the development of safety-critical automotive applications in an ISO 26262 context.
Why do software engineers – new and old – choose Ada and AdaCore tools?
Software is more and more important in many industrial applications. It can be a real differentiator for companies who want to offer new, more complex features. Dealing with this complexity, ensuring that the software does what it should do (and does not do what it is not supposed to do), brings many complications and challenges. Programming languages and accompanying tools can provide concrete solutions and ensure safe and reliable running of the overall application. What seemed like science fiction 15 years ago is now becoming a reality.
Is it true Ada community continues to grow in number and reach?
Yes, it is. We can’t talk about a lot of customer projects in our traditional A&D markets but this year we have five customers that either chose to adopt or switched from using other languages to Ada and SPARK because of the advantages when building reliable, safe, and secure software. One such example is the company Scandinavian Real Heart AB in Sweden; they are using a suite of AdaCore software solutions to develop reliable safety-critical embedded software for its revolutionary Total Artificial Heart.
Ada programmers were out in large numbers at the March for Science in the U.S., , including a group of female software engineers who formed FutureAda.org and Girls Code. Are you seeing more women getting involved?
I think the critical software development segment echoes the more general computer industry in the relatively small proportion of female software engineers. This trend is changing, and AdaCore has a number of women amongst its technical staff, but far too slowly for my liking.
No, they are doubling them – from what I’m seeing at various conferences around the globe.
It really isn’t an easy job. For example, finding the right balance between a car that moves at 5 miles per hour (mph) and halts every time it comes into contact with a potentially dangerous object and one that drives normally, properly taking into account all the factors in a normal road environment, is a very difficult task. Fortunately, a lot of these projects are applying proper software engineering principles and verification procedures to ensure that accidents and fatalities rest few and far between.
Are they seeking out more safety and security solutions, including software development environments and test/verification tools used in safety-critical/life-critical markets, including aerospace & defense?
AV projects are complex at many levels, not least the software. Ada and SPARK can provide quality guarantees that are more difficult to obtain using other languages. Combine the need to address security needs and we are uniquely positioned to offer solutions for building the most critical software. After all, our customers have been using the language and our toolset for decades doing just that.
We are certainly seeing evidence that more and more industries are coming to AdaCore to take advantage of the time-tested and trusted solutions used by customers in A&D.
We have a number of automotive customers that are exploring the benefits they achieve when using Ada and SPARK. We hope to see soon a deployed autonomous driving system built in Ada and/or SPARK.
Wind River’s Chip Downing has recommended AV companies learn from the aviation community, which has a long track record for safety. Do you agree?
I fully agree with Chip; there is no need to reinvent the wheel. DO-178 and EN 50128 have been very successful standards in producing software that doesn’t fail. Certain unmanned aerial vehicles (UAVs) already have to conform to DO-178 as they fly through public airspace.
Driverless trains in metro systems in Europe have to conform to EN 50128 as they are carrying passengers and interacting in an environment in the same way a train with a human driver would. I’d like to see this principle being applied to other domains that are currently self-regulated to ensure the reliable running of AV software systems protecting the users and those around them.
