Exhibition category
Main exhibits 1
GNAT Pro is Ada/C/Rust development solution for projects requiring certification DO-178C.
GNAT Pro Assurance is a tool suite that supports Ada, C/C ++/Rust languages and includes a configurable runtime library for highly reliable systems. Sustained branching (fixed version) service is provided for long-term projects, allowing continued use of the same version. Runtime library certification materials are also available to simplify development and verification work when obtaining certification, as well as certification materials for the tools.
Prevent Security Vulnerabilities Earlier
GNAT Pro Assurance customers can request a detailed list of known problems, each keyed to The MITRE Corporation’s Common Vulnerability Enumeration (CVE) database. Vulnerability reports are provided in machine- and human-readable reports. In addition to this, AdaCore produces Software Bills of Materials (SBOMs) supplied in the industry-standard Software Package Data Exchange (SPDX) format, allowing automated incorporation into customers’ vulnerability management and reporting systems.
Main exhibits 2
SPARKPro is tool Suite for the formal methods to improve safety and reliability. DO-333/DO-178C
SPARK Pro is a formal verification tool that realizes zero error in code by writing verification code based on specifications, and it is possible to write reliable code using theorem proving. Verification is a combination of static and formal verification, and is performed in three stages (confirmation of coding conventions and dependencies by flow check, and formal verification with contracts).
Features.
-Data flow analysis.
SPARK Pro detects programming errors that cause uncertainty or incorrect behaviour, such as references to uninitialised variables. Data flow analysis analyses access to global variables and allows you to check that your software complies with design specifications.
-Information flow analysis
Dependencies can be specified to limit the information flow (use of global variables and parameters by subprogrammes) allowed in a programme. Dependency violations (can be detected without having to compile the code).
-Exclusion of run-time exceptions.
By ensuring that the programme is free of run-time exceptions such as zero division, numeric overflow, buffer overflow, out-of-range indexing of arrays, etc., the mathematical proof (PROOF) guarantees this analysis. Thus, errors that are difficult to detect can be excluded when writing the programme.
-Property checks.
Safety and security properties can be written in the same format as used in Ada 2012 (subprogramme pre-conditions and post-conditions).
Using mathematical proofs, the SPARK Pro toolset can automatically verify that properties are satisfied for all possible input and execution paths a programme can take.
-Functional correctness.
The extended verification functionality permits the description of formal specifications of the behaviour (specification of requirements) required of a programme; SPARK Pro proves that the programme satisfies its functional specification. This provides assurance for critical system behaviour.
Main exhibits 3
Japanese Specification Document Review Tool Cyclo.Req
Cyclo.Req analyzes Japanese specification documents and points out ambiguities and syntax errors. Cyclo.Req also checks for specification omissions and inconsistencies by displaying state transition diagrams and simulations (behavior checking) to ensure that Japanese descriptions are suitable for program development before writing programs. AdaCore SPARK Pro and GNAT Pro are used for simulation.