安全規格のツール資格　ならびに　認証取得資料

AdaCore社は長年セーフティ・クリティカル・ソフトウェア開発用のソフトウェアツールを提供しています。各分野の安全規格の認証を取得するために、システムソフトウェアの実装、検証、保守を行うために各製品が利用されています。

安全規格のツール資格ならびに認証取得資料に関して

認証資料

AdaCore社は設立以来、厳格な安全性が要求される業界のお客様に各種サービスを提供しています。この経験により、DO-178B/C（航空）、EN 50128（鉄道）、ECSS-E-ST-40C / ECSS-Q-ST-80C（宇宙）、IEC 61508（産業）、ISO 26262（自動車）を含む主要なソフトウェア安全認証規格の深い専門知識を取得できました。AdaCore社のツールと技術は、機能性と安全性の両方の観点から、認証要件を満たしています。

Adaランタイムライブラリとコンパイラの認証エビデンス

GNAT Proツールチェーンには、no-run timeプロファイル（ゼロフットプリント）から最小限の機能セット（RavenscarタスクまたはCert/Minimalプロファイル）まで、認証を取得するアプリケーションに組込可能な各種ランタイムプロファイルが用意されています。各プロファイルを実装したコードは、DO-178B/CやEN-50128などの上位レベルの認証を対象とした成果物として利用できます。

さらにランタイムライブラリに加えて、コンパイラの認証エビデンスが必要な安全規格向けに以下の資料を用意しています。

• DO-178B/CレベルA認証ソフトウェアに必要なソース‐オブジェクト間のトレーサビリティ資料
• EN 50128の場合は、T3資格認定キット

 

GNAT Pro Assurance 認証取得向けツールチェーン

認証規格では、ソフトウェアを開発するために使用されるツールについて、特殊な管理/コンフィグレーションマネージメントが要求されます。ツール（特にコンパイラ）に問題点がある場合は、修正をただちに行い、認定ソフトウェアの開発/保守中には、再度の解析が求められます。GNAT Pro Assuranceが提供するSustained Branchサービスは、このニーズに対応するために、バージョンを固定して長期的なサポートが可能で、最初のリリースから何年か経過してからの修正や、既知の問題に対する追加の修正、インパクト解析（impact analysis）が含まれています。

 

 

資格認定取得済み検証ツール

認証要件に対応できる検証ツールが提供されており、DO-178C（TQL-5/TQL-4）、EN 50128（T2）などの認証プロセスでは、そのツールを使用して、手動での検証を省略することができます。　以下のツール認定ドキュメントが用意されています。

• GNATcheck, コーディング規格検査
• GNATcoverage, コードカバレッジ
• GNATstack, スタック消費の最大量の予測
• CodePeer, 脆弱性解析
• SPARK Pro, 形式検証

Simulink®用の認定コードジェネレータ

Simulink®モデリング言語用オートコードジェネレータはSimulink®からSPARK（Adaのサブセット）あるいはC言語ソースコードを生成します。　ソースコードは組込ターゲットで動作させるためにコンパイル可能です。生成されたソースコードの信頼度は、手動で検証するか、認定コードジェネレータを検証することで取得できます。AdaCore社QGenは、Simulink®からSPARK （Ada言語のサブセット）やMISRA Cへのコードジェネレータで、DO-178C TQL1やEN-50128 T3の認定資料を用意しています。

参考文献:AdaCore Technologies for EN 50128,AdaCore Technologies for DO-178C / ED-12C.