アイティアクセス株式会社

2024年10月吉日

2024国際航空宇宙展 出展のご案内

アイティアクセス株式会社は、2024/10/16（水）-10/18（金）の3日間
2024国際航空宇宙展
に出展することになりましたので、ここにご案内申し上げます。
今回は下記にご案内させて頂く製品群の展示を予定しております。
是非とも弊社ブースにお立ち寄りくださいますようお待ち申し上げております。

記

開催概要

■名称	2024国際航空宇宙展 JAPAN INTERNATIONAL AEROSPACE EXHIBITION 2024
■会期	トレードデー 10月16日（水） 12:00～17:00 10月17日（木）～18日（金） 10:00～17:00 トレード・パブリックデー 10月19日（土） 10:00～17:00
■会場	東京ビッグサイト 西展示棟 全館 ※小間番号W1-060
■入場料	トレードデー（要登録） ［会期前登録：10月15日まで］ 無料 ［会期中登録：10月16日以降］ 一般 5,500円（税込）
■主催	一般社団法人日本航空宇宙工業会 株式会社東京ビッグサイト

 

「出展の見どころ」

• DO-178C認証取得対応コンパイラ　GNAT Pro Assurance for Ada,C/C++, Rust 

認証取得ならびに長期にわたるプロジェクト対応

GNAT Pro Assuranceは、高信頼性、長期保守、ならびに認証取得が必要なプロジェクト向けソフトウェア開発ソリューションです。

本製品は、Ada言語規格（Ada 83からAda 2012まで）ならびにC（C11規格）およびC ++（C ++ 17規格）に対応、高信頼性システム用に構成変更可能なランタイムライブラリを提供するツールスイートです。昨年、RUSTにも対応しました。

GNAT Pro Assurance製品には、製品自身の問題点を修正するためにサステインド・ブランチ（Sustained Branches）と呼ばれるサービスが提供され、同一バージョンの使用を継続することができます。

AdaCoreは、認証を取得されるお客様へ長期にわたり製品、サービスを提供しています。GNAT Pro Assuranceには、開発と検証作業を簡素化できるオプション、ランタイムライブラリ認証資料や、ツールの認定資料なども用意されています。

DO-178C認証取得時に必要なスタック解析、Traceability Analysis レポートを作成可能です。

• 航空機のソフトウェアの安全性を向上させる形式検証ソフトウエアツール　SPARK Pro

より安全なコードを記述するために

SPARK Proは、形式検証可能なAda 2012サブセットの言語で、ソフトウェア検証に数学ベースの信頼性をもたらすツールセットです。

特長 

🔹データフロー解析

SPARK Proは、非初期化変数の参照など、不確実性や不正な動作の原因となるプログラミングエラーを検出します。 データフロー解析は、グローバル変数へのアクセスを解析し、ソフトウェアが設計仕様に準拠しているかを確認できます。

🔹インフォメーションフロー解析

依存関係を指定して、プログラムで許可されるインフォメーションフロー（サブプログラムによるグローバル変数とパラメーターの使用）を制限できます。依存関係違反は、コードをコンパイルしなくても検出可能です。

🔹実行時例外の除外

プログラムにゼロ除算、数値オーバーフロー、バッファオーバーフロー、配列の範囲外インデックスなどの実行時例外がないことを確認して、数学的証明（proof）は、この解析を保証します。そのため、プログラム記述時に、検出が困難なエラーを除外できます。

🔹プロパティチェック

セーフティやセキュリティプロパティは、Ada 2012で使用されているのと同一書式で記述できます（サブプログラムの事前条件と事後条件）。

数学的な証明を使用して、SPARK Proツールセットは、プログラムが取りうるすべての入力と実行パスについて、プロパティを満足するかを自動的に検証可能です。

🔹機能の正確さ

拡張された検証機能により、プログラムに要求される挙動の形式仕様（要件の仕様）の記述を許可します。SPARK Proは、プログラムがその機能仕様を満たしていることを証明します。これにより、クリティカルなシステムの動作に対して保証します。

CWE互換ツール

SPARK Proは、MITREのCommon Weakness Enumeration（CWE）互換性および有効性プログラムによりCWE互換として指定されており、CWEの上位25に指定されるソフトウェアエラーを検出できます。

• 自然言語ソフトウェア仕様書の日本語検証ツール Cyclo.Req

Cyclo.Reqは自然言語で記述された仕様書などを解析して、曖昧さや構文エラーなどを指摘します。さらに日本語記述がプログラム開発に適しているかを状態遷移図表示、シミュレーション（振舞検査）などを通して仕様漏れ、矛盾などがないかをプログラム記述前に検査できます。シミュレーションにはAdaCore SPARK Pro / GNAT Pro を使用します。