Ada Resource Association

AdaCore has released new versions of all of their products, include GNAT Pro, SPARK Pro, and CodePeer.

AdaCore publisizes the successful completion of a research project for DENSO, Application of Formal Methods to Help Achieve Freedom from Interference. This project, conducted jointly with the University of Nagasaki, had the goal of simplifying the development of safety-critical automotive applications in an ISO 26262 context.

In response to evolving requirements from existing customers and increasing interest in Ada from traditionally C-based application domains, AdaCore has launched three product lines for its GNAT Pro technology:

• GNAT Pro Enterprise, a full-featured environment supporting industrial-grade development of mission-critical software;
• GNAT Pro Assurance, an extension of GNAT Pro Enterprise oriented towards users with software certification requirements or the need for a stable development platform that is maintained (with repairs to critical issues) over the entire duration of a long-lived project; and
• GNAT Pro Developer, geared towards new users of Ada who want to take advantage of the language’s software engineering support and early error detection.

MDA, a business unit of Maxar Technologies, has selected the GNAT Pro Assurance Ada development environment for the LEON3 target processor, to produce the software for a Ku-Band communication subsystem that will replace the current version. This critical International Space Station (ISS) subsystem has to work reliably over the long term, a requirement that led MDA to maintain Ada as the implementation language.

AdaCore today announced that its GNAT Pro Ada environment has been successfully used by Thales to develop and verify a qualified autocode generator for critical airborne software. Thales implemented the autocode generator in Ada; the tool takes an XML file and produces source code for an embedded avionics system that will be assessed against the Level B objectives in DO-178C / ED-12C.

AdaCore today announced the winners of its second annual Make with Ada programming competition for embedded projects. Make with Ada aims to show how the Ada and SPARK language technologies can significantly improve code quality for modern embedded systems without requiring a steep learning curve for developers unfamiliar with these languages. Prizes are awarded to the projects that best meet the overall criteria of software dependability, openness, collaborativeness and inventiveness.

Read the linked press release for the details.

The GNAT Pro Ada Development Environment is available the Wind River® FACE Certified VxWorks® 653 Platform. In addition, AdaCore has initiated the FACE verification/certification process for GNAT Pro. VxWorks 653 is the first Commercial-Off-The-Shelf (COTS) product to be certified as conformant to the FACE Technical Standard’s Operating System Segment (OSS) Safety Base Profile.

MHI Aerospace Systems Corporation (MASC) has selected the QGen toolset to develop the software for the Throttle Quadrant Assembly (TQA) system. This avionics research project is being conducted to meet the Level C objectives in the DO-178C safety standard for airborne software and its DO-331 supplement on Model-Based Development and Verification. The use of a qualified code generator can help save significant effort in developing and verifying the software, and the future availability of qualification material from AdaCore factored strongly in MASC’s decision to choose QGen. The QGen code generator can be qualified at the highest Tool Qualification Level, TQL-1 (equivalent to a development tool in DO-178B).

AdaCore today launched its 2nd annual “Make with Ada” programming competition, a contest that aims to help the embedded software community improve the quality of their code by encouraging the use of the Ada and SPARK programming languages. The competition runs from May 15 to September 15, 2017, and offers over €8000 in total prizes. Participants can register for the competition at .

A free booklet, co-authored by AdaCore and Thales, explains how to exploit SPARK/Ada technology to achieve high levels of software assurance. The booklet, Implementation Guidance for the Adoption of SPARK, which explains how best to introduce and make use of the SPARK/Ada formal verification technology based on a project’s assurance goals. It explains the associated benefits and costs at each level, and details the processes that Thales is using to introduce formal verification in operational projects. The booklet will be a valuable resource for anyone responsible for producing high-assurance software for critical systems.