Developing high integrity software at the highest level of safety (ASIL-4) requires the introduction of expensive specification and verification techniques. C and C++ as programming languages aren’t designed to accompany these processes and requires a lot of tooling and work to achieve the right level of confidence. This webex will develop an alternative approach based on the Ada programming language and the SPARK formal proof enfornment, showing how using coding techniques built for verification can reduce high-integrity software development and increase overall reliability and time-to-market.
– Overview of the Ada and SPARK programming languages
– Understanding Formal Proofs and how they differ from traditional static analysis
– Mixing Ada and SPARK together with legacy C code
– ISO-26262 considerations and benefits
– Industrial references

Presented by Michelle Ricardo, AdaCore
From Tech Days Boston, 2019

Presented by Abe Cohen at AdaCore Tech Days Boston, 2019.

Presented by Robert Tice at AdaCore Tech Days Boston, 2019.

Presented by Quentin Ochem at AdaCore Tech Days Boston, 2019.

Presented by Arnaud Charlet at AdaCore Tech Days Boston, 2019.

Presented by Tony Aiello at AdaCore Tech Days Boston, 2019.

Presented by Raymond Richards, Darpa/I20 — at AdaCore Tech Days Boston, 2019.

Presented by Michael Frank at AdaCore Tech Days Boston, 2019.

Presented by Quentin Ochem at AdaCore Tech Days Boston, 2019.

A research and development project by AdaCore in collaboration with the Air Force Research Laboratory.

Presented by Tony Aiello at AdaCore Tech Days Boston, 2019.

GNATtest helps automate the essential, but tedious and error-prone, processes for developing and managing the large number of test cases needed for verifying large software systems.

Learn more at https://www.adacore.com/gnatpro/toolsuite/gnattest

Get an intro to ARINC 653 + DO-178C/ED-12C, and demos on using various tools from AdaCore and Wind River including:
- Wind River VxWorks 653 3.1.3
- GNATbench 18.2

Sensor fusion software is unique with its combination of firmware-like layers, responsible for reading and validating sensor data, and higher-level algorithmic software, responsible for producing synthesized, actionable data. Because of the criticality of these systems, they require extensive testing and verification to increase confidence that the computed data can be trusted. From a software development point of view, the traditional approach is to rely on the C or C++ programming language, and to offset its inherent safety vulnerabilities by using expensive tooling and human-based processes. In this presentation we will present an alternative approach, through the usage of a different programming language which was designed for safety critical systems and gives developers tools to write safe and secure firmware, as-well-as, robust high-level algorithmic code with the same ecosystem of language and tooling. Topics covered:

- Overview of Ada and SPARK language features for firmware development
- Overview of Ada and SPARK language features for algorithm and high-level software development
- Overview of formal proof and how it differs from traditional static analysis techniques
- Integration with existing C code bases
- Performances considerations
- ISO 26262 considerations and benefits
- Resources for Ada and SPARK in the software community

As software becomes more complex, the chances of human error greatly increase, opening up potential for security and safety risks. NVIDIA is working with AdaCore to implement Ada and SPARK programming languages into certain firmware elements to reduce this potential error. In this webinar you will learn how the combination of NVIDIA hardware with Ada and SPARK delivers robustness and security, improving efficiency and safety in the development pipeline.

(re-upload to fix some audio issues)

As software becomes more complex, the chances of human error greatly increase, opening up potential for security and safety risks. NVIDIA is working with AdaCore to implement Ada and SPARK programming languages into certain firmware elements to reduce this potential error. In this webinar you will learn how the combination of NVIDIA hardware with Ada and SPARK delivers robustness and security, improving efficiency and safety in the development pipeline.

0:00 - Intro by Patrick Mannion
2:10 - Business context for Ada and SPARK at NVIDIA by Daniel Rohrer
18:41 - Technical aspects of NVIDIA's adoption of SPARK by Dhawal Kumar
19:33 - Firmwares and their environment
21:01 - What is this SPARK that we've all been raving about?
29:35 - SPARK aternatives considered (and dismissed)
36:35 - Proof of Concept — It's conclusions and concerns
45:38 - Benefits and Summary
48:37 - Q and A

GNAT Pro is a robust and flexible Ada, C and C++ development environment. It comprises a toolchain based on the GNU GCC technology; an Integrated Development Environment (GNAT Studio); a comprehensive toolsuite, including a visual debugger; and a set of libraries, bindings and tools.

GNAT Pro is upgraded annually, and Version 21.0, released earlier this month, adds support for a number of new platforms, including VxWorks 600+ on x86 / ARM / PowerPC; C++ availability on all VxWorks 7 ports; Windows-hosted Linux cross for ARM (PowerPC is also available); and RISC-V 32 on bare metal. Version 21.0 also adds a number of key features, including a more powerful CCG (Common Code Generator), new Libadalang capabilities for Ada code analysis, and support for key features of the Ada 202X standard. All of these upgrades are designed to better support multi-language and safety-critical development as well as security vulnerability resilience.

Check out this video to learn how GNAT Pro’s new platforms, tools and libraries can help kick your workflow up to the next level.

GNATcoverage is an all-in-one code coverage analysis tool. It thoroughly tracks the execution of your program and records this information in a trace file.

This year, GNATcoverage offers source code instrumentation capabilities that make code analysis more accessible, more versatile, and much, much faster on native platforms. It also allows the technology to be used across the board, alongside on all targets and all versions of the GNAT Pro technology.

We’re excited to show you what GNATcoverage can do. Check out this video to learn just how easy GNATcoverage is to use, and how the new capabilities can help you meet the highest software quality standards.

SPARK Pro is a language and toolset that allows developers to formally define and automatically verify software requirements to guarantee that a program behaves as intended. You can adopt SPARK either at the beginning of a project, or by progressively integrating it in an existing codebase developed, for example, in Ada, C or C++.

AdaCore’s release of SPARK Pro 21.0 expands its support of Ada language constructs, allowing more programs to be effectively specified and verified, and provides better tool interactions with improved tool messages and guidance.

Check out this video to discover how the latest capabilities in SPARK 21.0 can help you save time and effort while reaping the full benefits of formal program verification.