出展カテゴリー
連絡先
| 住所 | 横浜市港北区新横浜3-17-6 |
|---|---|
| 電話番号 | 0454749095 |
| URL | https://www.itaccess.co.jp/service/adv/brand/adacore/ |
| itainfo@itaccess.co.jp |
主な出展物1
DO-178C認証取得対応コンパイラ GNAT Pro Assurance for Ada,C/C++, Rust
認証取得ならびに長期に渡るプロジェクト対応。
GNAT Pro Assuranceは、高信頼性、長期保守、ならびに認証取得が必要なプロジェクト向けのAda開発ソリューションです。
本製品は、Ada言語規格（Ada 83からAda 2012まで）ならびにC（C11規格）およびC ++（C ++ 17規格）に対応、高信頼性システム用に構成変更可能なランタイムライブラリを提供するツールスイートです。昨年、RUSTにも対応しました。
GNAT Pro Assurance製品には、製品自身の問題点を修正するためにサステインド・ブランチ（Sustained Branches）と呼ばれるサービスが提供され、同一バージョンの使用を継続することができます。
AdaCoreは、認証を取得されるお客様へ長期にわたり製品、サービスを提供しています。GNAT Pro Assuranceには、開発と検証作業を簡素化できるオプション、ランタイムライブラリ認証資料や、ツールの認定資料なども用意されています。
DO-178C認証取得時に必要なスタック解析、Traceability Analysis レポートを作成可能です。
主な出展物2
航空機のソフトウェアの安全性を向上させる形式検証ソフトウエアツール SPARK Pro ( DO-333/DO-178C)
より安全なコードを記述するために
SPARK Proは、形式検証可能なAda 2012サブセットの言語で、ソフトウェア検証に数学ベースの信頼性をもたらすツールセットです。
特長
🔹データフロー解析
SPARK Proは、非初期化変数の参照など、不確実性や不正な動作の原因となるプログラミングエラーを検出します。 データフロー解析は、グローバル変数へのアクセスを解析し、ソフトウェアが設計仕様に準拠しているかを確認できます。
🔹インフォメーションフロー解析
依存関係を指定して、プログラムで許可されるインフォメーションフロー（サブプログラムによるグローバル変数とパラメーターの使用）を制限できます。依存関係違反（は、コードをコンパイルしなくても検出できます。
🔹実行時例外の除外
プログラムにゼロ除算、数値オーバーフロー、バッファオーバーフロー、配列の範囲外インデックスなどの実行時例外がないことを確認して、数学的証明（proof）は、この解析を保証します。そのため、プログラム記述時に、検出が困難なエラーを除外できます。
🔹プロパティチェック
セーフティやセキュリティプロパティは、Ada 2012で使用されているのと同一書式で記述できます（サブプログラムの事前条件と事後条件）。
数学的な証明を使用して、SPARK Proツールセットは、プログラムが取りうるすべての入力と実行パスについて、プロパティを満足するかを自動的に検証可能です。
🔹機能の正確さ
拡張された検証機能により、プログラムに要求される挙動の形式仕様（要件の仕様）の記述を許可します。SPARK Proは、プログラムがその機能仕様を満たしていることを証明します。これにより、クリティカルなシステムの動作に対して保証します。
CWE互換ツール
SPARK Proは、MITREのCommon Weakness Enumeration（CWE）互換性および有効性プログラムによりCWE互換として指定されており、CWEの上位25に指定されるソフトウェアエラーを検出できます。
主な出展物3
自然言語ソフトウェア仕様書の日本語検証ツール Cyclo.Req
Cyclo.Reqは自然言語で記述された仕様書などを解析して、曖昧さや構文エラーなどを指摘します。さらに日本語記述がプログラム開発に適しているかを状態遷移図表示、シミュレーション（振舞検査）などを通して仕様漏れ、矛盾などがないかをプログラム記述前に検査できます。シミュレーションにはAdaCore SPARK Pro / GNAT Pro を使用します。
●複数視点からの検査
次に示す検査を通じて、読みやすさや正確さの検査を行います。この検査によって、修正が望ましい箇所を知ることができます。結果は、警告・確認・推奨のレベルに分けて出力します。
●検査
-文体（敬体／常体や句読点の使い分けなど）の検査をします
-読みやすさに影響する読みやすさ、助詞の使い方を検査します
-場合分けや、正確さに影響する言葉の検査を行います
-主語の有無や、述語項構造に基づき、述語に関する検査を行います
●文の構造
文の係受け関係を表示します。指摘の詳細を知る、或いは、対象文を修正するときに役立ちます。
●指標
検査に基づく各種の指標を得ることができます。指標から、より慎重に検査すべき文書が分かります。文書レビューにおいて、特に有効です。
●辞書
さまざまなユーザ定義辞書を持ちます（用語・定性的用語・口語表現・形式記述など）
この辞書記述をユーザの作業領域に合わせて、充実させることができます。結果として、より良い検査が可能となります。また、追加すべき未知語を、自動的に抽出します。用語への追加は簡単です。なお、自動車関連用語辞書を、標準で持っています。_