AdaCore + アビオニクス
AdaCoreは、アビオニクス業界のお客様に長年サービスを提供してきた実績を持つ企業です。同社の製品は、開発者が最高レベルの安全認証を満たすソフトウェアシステムを構築し、検証するのを支援します。
現在、世界中で毎日800万人以上の人々が民間航空機を利用しており、年間では30億人以上の乗客に達します。それにもかかわらず、空の旅は依然として最も安全な交通手段とされています。これは、アビオニクス業界が安全性と信頼性の高いソフトウェアを開発するために極めて厳格な要件を設定していることに大きく依存しています。
DO-178の要件を満たすことは、多くの場合、複雑でコストのかかるプロセスです。AdaCoreはアビオニクス業界のお客様との豊富な経験を通じて、認証プロセスの複雑さを深く理解し、ワークフローを簡素化しコストを管理するためのツールを提供しています。
認証のルーツ – DO-178B / DO-178CのレベルAとB
AdaCore社は、DO-178BおよびDO-178CのレベルAおよびBに関する認証プロセスに幅広い知識と経験を有しており、規格に関連するワーキンググループや委員会でも積極的に活動しています。AdaCoreの社長で共同創設者であるCyrille Comar博士は、ソフトウェア認定の専門家として高く評価されており、DO-178Cおよびその関連サプリメントの開発にも携わりました。
認定ツール、ランタイムライブラリ、および認定資料
AdaCoreのいくつかのツールは認定を受けており、コーディング標準への準拠、バッファオーバーランや整数オーバーフローなどのエラー防止、MC/DC（修飾条件/決定条件）の構造カバレッジ解析など、検証目標を達成する際の労力を軽減します。
さらに、Ravenscarタスクプロファイルを実装した高保証ランタイムライブラリは、認定システムに組み込むのに十分シンプルである一方、ハードリアルタイムのアビオニクスソフトウェアに求められる機能をサポートします。これらのツールとライブラリには認定資料も用意されており、新しいプロジェクトにも柔軟に適用可能です。
サステインド・ブランチ（Sustained Branch）サービス
認定ソフトウェアの保守には、特定のバージョンを「固定（フリーズ）」する必要があり、安定性を維持するための独自の課題が伴います。しかし、ソフトウェアの進化に伴い問題が発生した場合には、更新されたリリースが必要となる場合もあります。
AdaCoreの「サステインド・ブランチ」サービスは、このような課題に対応するために提供されており、DO-178B / DO-178Cのガイダンスに沿った形でこの要件をサポートしています。このサービスは、GNAT Pro保証製品の標準的な一部として提供されています。
————————————————————————————————————————————————————————————————————————–
AdaCoreは、DO-178B/C認証のコスト削減やワークフローの効率化を支援するさまざまなツールとサービスを提供しています。その中心となるのが、重要なシステム向けに特化したAda開発環境「GNAT Pro Assurance」です。
————————————————————————————————————————————————————————————————————————–
GNAT Pro Assuranceには、「サステインド・ブランチ」と呼ばれる専門サービスが含まれており、プロジェクトで使用する特定の技術バージョンを安定的に維持しつつ、重要な問題を修正するためのアップグレードが可能です。この環境は、Ada言語の全バージョンをサポートし、オプションでC言語サポートも追加できます。
さらに、GNAT Pro Assuranceには完全なツールスイートが含まれており、構成可能なランタイムライブラリや、高保証システムに特に適した専用ランタイムライブラリも提供されています。
SPARK Proは、安全性やセキュリティが最優先されるアプリケーションの開発に特化した言語およびツールセットです。このツールセットは、高い信頼性、低い誤警報率、深い静的検証を実現し、安全性やセキュリティに関する認証要件を満たすための正確な証拠を生成します。
GNAT SASは、開発者がコードを深く理解し、信頼性が高く安全なソフトウェアを構築するための支援を行うAdaソースコードアナライザーです。このツールは、ランタイムエラーやロジックエラーを検出し、プログラム実行前に潜在的なバグや脆弱性を評価します。
GNAT SASは、自動化されたピアレビュー機能としても機能し、開発ライフサイクルのどの段階でもエラーを容易に発見できます。これにより、コードの品質向上や安全性・セキュリティの分析が効率化されます。
GNAT Coverageは、オブジェクトコード（命令および分岐カバレッジ）とAdaやC言語のソースコード（ステートメント、決定、修飾条件/決定カバレッジ – MC/DC）の両方についてカバレッジ分析を行います。これにより、ソフトウェアの動作やテストの完全性を詳細に評価できます。
DO-178C / ED-12CとAdaCoreの技術
DO-178C / ED-12C規格のガイダンスと、技術固有の補足資料は、航空機搭載ソフトウェアがその要件を満たしていることを証明するための重要な指針を提供します。このガイダンスへの準拠を証明することは特に検証活動において困難を伴いますが、認定ツールや専用ランタイムライブラリを適切に活用することで、作業を大幅に効率化することが可能です。
本資料では、AdaCoreが提供する各種テクノロジー（ツール、ライブラリ、補足サービス）が、このプロセスをどのように支援できるかを解説します。
ダウンロード【英語版】
AdaCoreDO178C*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文こちらをご参照下さい。
