2025/6/2

高信頼性ソフトウェアツールの開発において業界をリードするAdaCoreは、AdaおよびSPARKプログラミング言語を自動車分野に本格導入することを発表いたしました。

本取り組みは、パートナーであるNVIDIAとの協業により実現したもので、他の企業が容易に追随できる「直ちに利用可能なリファレンスプロセス」の提供を通じて、業界全体への普及を目指します。

NVIDIAは、自動運転車向けアプリケーションの開発・展開を目的に、同社のDRIVE AGXプラットフォーム上で動作するリファレンス・オペレーティング・システムおよびソフトウェア・スタック「Drive® OS」を開発しました。

本システムには、自動車向け機能安全規格「ISO 26262」において、最高レベルの安全要件に準拠したソフトウェアコンポーネントが含まれています。こうした高度な安全基準を満たすため、NVIDIAはソフトウェア・スタックの中でも特に重要なコンポーネントに、AdaおよびSPARK言語を採用しました。これにより、形式手法（フォーマルメソッド）をはじめとする両言語の特性を最大限に活用した、安全性を重視した開発プロセスの確立が可能となりました。

AdaCoreとNVIDIAは、リファレンスプロセスをオープンソースとして無償で公開し、あらゆる開発者や企業が自由に利用・カスタマイズできる形で提供しています。これにより、自動車業界全体におけるAdaおよびSPARK言語の普及と、安全性を重視したソフトウェア開発の促進を目指しています。

AdaCoreの最高製品・収益責任者（Chief Product and Revenue Officer）であるクエンティン・オケム（Quentin Ochem）氏は次のように述べています。

「自動車業界における付加価値は、従来の機械的要素からソフトウェア機能へと大きく移行しています。これに伴い、ソフトウェアの安全性をいかにして確保するかが、現代の車両開発における最重要課題の一つとなっています。NVIDIAは、開発プロセスにAdaおよびSPARK言語を導入し、その取り組みを他の開発者が参照可能な形で公開することで、この分野における優れた技術的リーダーシップを示しています。」

ISO 26262準拠のリファレンスプロセスは、以下のURLより無償で入手・カスタマイズが可能です：

• https://nvidia.github.io/spark-process/
• https://github.com/NVIDIA/spark-process

AdaおよびSPARK言語を学べるインタラクティブな学習プラットフォームをぜひご覧ください。

Learn Ada Today

Visit our interactive platform designed to teach the Ada and SPARK languages. »

AdaCoreについて

1994年に設立されたAdaCoreは、ミッション・クリティカル、セーフティ・クリティカル、かつセキュリティ・クリティカルなシステム向けにソフトウェア開発・検証ツールを提供しています。

長年にわたり、AdaCore製品を利用されているお客様は、セーフティ・クリティカルなアプリケーションを開発し、保守を継続されています。その分野は、商用航空機、自動車、鉄道、宇宙、軍事、航空交通管制、医療機器、財務サービスなどです。AdaCore社の顧客は、世界的に幅広い分野で増え続けています。詳細については、こちら（英語）をご覧ください。

AdaCore製品はオープンソースで、開発エンジニア自身が専門的なオンラインサポートを提供しています。同社の拠点は、ニューヨークならびにパリにあります。

AdaCoreホームページ

※本資料は、AdaCoreのプレスリリースを意訳したものです。正確な内容については、原文こちらをご参照下さい

メモリ・セーフティに関わるバグは、ソフトウェアのセキュリティや信頼性に深刻な影響を与える原因となります。実際、Google や Microsoft などの大手テクノロジー企業は、報告されているセキュリティ脆弱性の70％以上が、こうした問題に関連しているとしています。これらのリスクを効果的に減らすためには、プログラミング言語の設計段階でメモリ・セーフティを確保することが非常に重要です。
本ホワイトペーパーでは、境界外書き込みやユーズ・アフター・フリー、ヌル・ポインタ参照といった、よく見られるメモリ・セーフティのバグについて説明します。あわせて、Ada、SPARK、Rust といったプログラミング言語が、これらの問題にどのように対応しているのかを解説します。

[日本語版]　ダウンロード

[原文　英語版]　ダウンロード

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

2025年5月吉日

人とくるまのテクノロジー展 2025 YOKOHAMA 出展のご案内

アイティアクセス株式会社は、2025年5月21日（水）～ 5月23日（金） 3日間
人とくるまのテクノロジー展 2025 YOKOHAMA
（2025年5月14日（水）～ 2025年6月4日（水）はオンライン展示会）
に出展することになりましたので、ここにご案内申し上げます。
今回は下記にご案内させて頂く製品群の展示を予定しております。
是非とも弊社ブースにお立ち寄りくださいますようお待ち申し上げております。

記

開催概要

「出展の見どころ」

• 安全なソフトウェア開発ツール　SPARK 

プログラムを形式記述できるSPARKは、静的解析/形式検証ツールとともの統合され、安全なコードを生成し脆弱性を回避できます。 

SPARK Proは、仕様と実装を形式記述して整合性を検証するツールで、コードのエラーゼロを目指します。定理証明が活用できるため、高い信頼性を持つソフトウェアの開発が可能になります。 

検証は以下の3段階で行われます： 

1．コーディング規約のチェック 

2．フローチェックによる依存関係などの確認 

3．事前、事後条件を活用した形式検証 

このように静的検証と形式検証を組み合わせることで、SPARK Proはメモリの安全性、サイバーセキュリティ対策、脆弱性の防止といった分野で有効に活用できます。 

• メモリ保護の強力な開発言語　Rust 

Rustを使用する、変数の所有権、借用といった機能により、メモリの保護が強力で、安全なプログラムを生成することができます。 

GNAT Pro Assuranceは、Rust（強力なメモリ保護機能対応）、Ada、C/C++といった言語に対応した、高信頼性システム向けのツールスイートです。構成可能なランタイムライブラリを含んでおり、厳しい要件のシステム開発に柔軟に対応できます。 

長期プロジェクトにおいては、特定のバージョンを固定して継続使用できるバージョン固定サービスが提供されており、安定した開発環境を維持可能です。 

さらに、認証取得に必要な開発・検証作業の負担を軽減するために、ランタイムライブラリの認証資料やツールの認定資料も充実しています。 

• 仕様書（自然言語）検証ツール　Cyclo.Req 

Cyclo.Reqは、日本語（自然言語）で記述された文書を解析し、曖昧さ、構文エラーを指摘するツールです。仕様書から形式検証コードを生成して、振舞検査を行い、要件の確からしさも検証することができます。 

DO-178C/ED-12Cの正式名称は「Software Considerations in Airborne Systems and Equipment Certification」で、民間航空機に搭載されるソフトウェアの妥当性を規定する認証規格です。section1.1には次のように記載されています：
「この文書の目的は、耐空性要求に準拠し、確実な安全性で、その機能を達成する航空機システムおよび搭載機器用のソフトウェアを開発するためのガイダンスを提供します。」

このガイダンスは、次の内容で構成されています：ソフトウェアライフサイクルプロセス（software life cycle processes）に関連するobjective

• 計画プロセス（Planning process）
• 開発プロセス（要求、設計、コーディング、統合）　Development processes (requirements, design, coding, integration)
• インテグラルプロセス（検証、構成管理、品質保証、認証調整）Integral processes (verification, configuration management, QA, certification liaison)
• objective達成のための推奨アクティビティ（DO-178Cは、 software life cycle objectives に準拠するためのガイダンスと手法を示し、その手法を活用事例に当てはめることも推奨しています。）
• ソフトウェアライフサイクルデータ（Software life cycle data）：アクティビティ/objectivesが達成されたことを検証するエビデンス（「成果物」）。

ソフトウェア・レベルは、どのガイダンスが、どの程度厳密に適用されるかを定めています。また、ソフトウェア異常が耐空性／パイロットの業務負荷に与える影響に基づいており、安全性評価（system life cycle process）の中で決定されます。DO-178C/ED-12C規格でのソフトウェア・レベルは、D (軽微な障害状態につながる可能性) から A (壊滅的な障害につながる可能性） までの範囲です。その主な目的は検証プロセスで、検証はソフトウェアライフサイクルプロセス（software life cycle process）の成果物を技術的に評価することです。レビュー、解析、テストを通じてソフトウェア開発中に発生したエラーを検出し、報告します。

section6.3には以下のように記載されています：

• 「レビューは、妥当性を定性的に評価し 、チェックリストまたは類似した方法で、成果物を検証します。」レビューとは、DO-178C/ED-12C のobjectivesに準拠したソフトウェア開発によって作成された、ソフトウェア要求、ソフトウェア・アーキテクチャ、ソースコード、オブジェクトコード、テストなどのソフトウェアライフサイクルデータの評価を指します。
• 5.0 Software Development Processes
• 6.4 Software Testing

レビューは認証で必要なエビデンスの必須項目です。具体的に、レビューはDO-178C/ED-12Cの以下のsectionに準拠しています

• 6.3 “Software Reviews and Analyses” and
• 6.4.5 “Reviews and Analyses of Test Cases, Procedures, and Results”).

以下のDO-178C/ED-12C sectionは、追加の「レビュー」アクティビティを定義していますが、ソフトウェア検証プロセスとは異なるため本稿の対象外です。

• 4.6 “Review of the Software Planning Process”
• 7.2.5 “Change Review”
• 8.3 “Software Conformity Review”

本稿は、DO-178C/ED-12Cの観点から効果的なレビューを行うためのフレームワークを定義し、活用する方法を紹介するブログの第1回目です。ツールのレビュー・フレームワークを実現する前に必要なステップは以下の通りです。

1. DO-178C/ED-12Cに規定または暗黙の内に示されているレビュー関連の制約を説明します。
2. DO-178C/ED-12Cに準拠したチェックリスト、レビュー権限、レビューアーの役割等で構成され、レビューに最低限必要なフレームワークを定義します。
3. GitLabなどの構成管理リポジトリを設定し、開発アクティビティを分析してライフサイクルデータを抽出します（プロジェクト、リポジトリ、継続的インテグレーションの自動化など）。GitLab CI（Continuous Integration）は、ソフトウェア開発プロジェクトのビルド、テスト、デプロイプロセスを自動化するためにGitLabに統合されたDevOpsツールです。

本稿では、DO-178C/ED-12Cのレビューobjectiveを効率良く達成するための制約（独立したエビデンスの記録、レビューする構成項目など）を特定します。続いて、2つの項目について説明します。

レビューについて

レビューの主な目的は、DO-178C/ED-12Cでは必須で、開発プロセスの初期段階で潜在的なソフトウェアの欠陥、エラー、不整合を特定し、修正することです。特に、アクティビティが自動化（認定された）ツールで実行されない場合に重要です。

DO-178C/ED-12Cのソフトウェアレビューアクティビティには、重要な要素が含まれています。

1. 3で説明されているように、技術データならびにライフサイクルデータを確認するためのチェックリストまたは類似の補助手段の使用。
2. ソフトウェア検証結果の作成（14に従ってレビューされたソフトウェアのレビュー記録と構成管理情報を含む）。
3. 0(b)に示されるレビューされたライフサイクルデータを効率的に保存および取得するためのメカニズムの導入。
4. 6ならびに6.2にあるように、独立した検証を実施すること。レビューは開発者以外の担当が行い、エビデンスは、出力からアクティビティと入力をトレースできる必要があります
5. section6.3.1から6.4.5で概説されているobjectiveに準拠するために、上位要求（high-level requirements）、下位要求（low-level requirements）、アーキテクチャ（architecture）、ソースコード(source code)、統合プロセス（integration process）の出力、およびソフトウェアテストアクティビティ（software testing activities）のレビュー。
6. section 11.14 に定める、不具合報告によるレビュープロセス中に発見された問題の記録。

DO-178C/ED-12Cのレビューの最初のタスクは、ソフトウェアライフサイクルデータ（software life cycle data）の8つのカテゴリーに分類されたレビューと解析のobjectivesに注目することです。

下図は、ソフトウェア検証プロセスにおいてレビューのために提出されるソフトウェアライフサイクルデータ（software life cycle data）の概要を示しています：

DO-178C/ED-12Cのsection6.3「Software Reviews and Analyses」とsection6.4.5「Reviews and Analyses of Test Cases, Procedures, and Results」には、31のレビューと解析objectivesが明示されています。そのため、レビューの目的は、Objectivesが達成されたことを明確にすることです。そして、適切な検証方法を選択し、検証対象に焦点を当てる必要があります。

検証手法について

レビュー vs 解析

先に示した方法論を適用するために、レビューまたは解析を通じて、すべてのsoftware life cycle data（上位要求(high level requirements)、下位要求(low level requirements)、ソフトウェア・アーキテクチャ、ソースコード、実行可能オブジェクトコード、テストケース、テスト手順、およびテスト結果など）が、Objectivesを達成していることを確認する必要があります。

解析は再現可能なエビデンスとして妥当性を示し、レビューは定性的に妥当性を評価します（DO-178C/ED-12C 6.3項）。レビューの工数を削減する一つの解決策は、DO-333/ED-216 「Formal Methods Supplement to DO-178C/ED-12C and DO-278A 」を用いて、レビューを形式手法で解析することで 補完または置き換えることができます。「形式手法はライフサイクルの初期段階でエラーを特定できるため、プロジェクト全体の工数を削減することができます。(DO-333/ED-216 Section FM.B.1.4.4 Reduce Effort)

例えば、「上位要求(high level requirements)が正確で、曖昧さがなく、詳細な」objectiveであれば、要求が形式記述されていれば、形式解析で処理することができます。また、「上位要求(high level requirements)が形式記述されていれば、正確で曖昧さはなくなります。さらに、上位要求(high level requirements)の形式モデルは、一貫性（矛盾のなさ）を確認することが可能で、形式解析を用いて正確性を検証することができます。」(DO-333/ED-216section6.3.1 b)。

実際に、従来のソフトウェア開発では、次のようになります：

• 上位要求(high level requirements)と下位要求(low level requirements)は自然言語で書かれています。
• ソフトウェア・アーキテクチャは、形式的または準形式的記述を用いないで設計されています。
• コードチェッカーツールを使用して、コーディングルールを検証します。（3.4-c Conformance to standard）
• 静的コード解析ツールを使用して、ソースコードの正確性と一貫性を確認します。（3.4-e Accuracy and consistency）

31個のDO-178objectiveのうち、29個以上のobjectiveがレビューによって検証されます。

形式記述では、次のようになります：

• 上位要求(high level requirements)は、制約のある自然言語（EARSなど）で記述されます。
• 下位要求(low level requirements)は、形式記述（例：SPARK、SPARKはAdaを基にした言語で、コントラクト（contract）や拡張アノテーションを通常のAdaコードのサブセットとして追加されています）で記述されます。
• 「要求を形式記述すると効率が良くなります。」（(DO-333/ED-216 Section FM.B.1.4.1 Improve Requirements)。
• ソフトウェア・アーキテクチャは、UMLのような準形式記述で設計されます。
• 設計検証ツールは、ソフトウェア・アーキテクチャの検証に使用されます（Simulink Design Verifier、GNATprove（データフローの正確性を検証するため）など）。
• 自動化されたドキュメンテーション生成ツールを使用して、トレーサビリティマトリクスを生成します。

準形式記述を用いると、検証するレビューobjectivesを減らしたり、工数を軽減したりすることが可能になります。さらに、規定や規則に従うことで、その柔軟性や解釈の幅が拡がります。この記述法は、必ずしも絶対的な正確さが要求されない場合や、形式記述と可読性を両立させる必要がある場合に用いられます。以下は、EARS構文を使用した例です（EARSはEasy Approach to Requirements Syntaxの略で、テキスト形式の要求を適切に制約するメカニズムです）。EARS 形式の構文は、体系化されたガイダンスを提供するため、品質の高いテキスト要求を記述できるようになります：

When the input A is below 20 [amperes] for more than 10 [milliseconds], the function B shall set the output C to ACTIVE

（入力Aが20 [アンペア]を下回る時間が10 [ミリ秒]を超える場合、関数Bは出力CをACTIVEに設定します。）

要約すると、評価を自動化（レビューを解析に切り替える）、または、形式あるいは準形式記述を用いることで、レビュープロセスを簡素化できます。

レビュー方法

DO-178C/ED-12Cでは、準拠すべき特定のレビュー方法を定めていません。ただ、「レビューは、チェックリストまたは類似した方法で示されたプロセスの成果物で検証を行います。」(6.3 Software Reviews and Analyses)。

代わりに、正確性、精度、完全性、検証可能性など、達成すべきobjectivesと基準（criteria）を規定しています。その結果、文書に定められた基準（criteria）を満たす限り、レビュー方法を選択することが可能になります。

一般的には、ウォークスルー（walk-through）とインスペクション（inspection ）という2つのレビュー方法を用います。２番目の方法は、問題点をより明確にしますが形式化が求められます。

ウォークスルー方式は一種の査読であり、成果物を複数の担当で確認します。ロジック、構造、機能を理解することに重点が置かれ、形式にとらわれず内容を理解することを目的としています。

インスペクション（inspection method）は、1970年代にマイケル・フェイガン氏（Michael Fagan）によって提唱された検査法で、より形式的なプロセスで、管理者（moderator）が複数のレビューアーとともに成果物をレビューします。あらかじめ定義された基準（criteria）または規格（standard）に従って、成果物を検証します。

課題

以下の点に注意することで、効率の低下や工数の増加を防止できます。最初の3つの制約は、構成の明確化、独立性、可用性です。

最後の3つは、工数を削減し、管理を容易するための手段となります。

構成の明確化

DO-178C/ED-12Cでは、レビューした構成項目を明確化することが重要です。

• 開発プロセス全体を通してトレーサビリティを確保するために、要求、テスト、レビュー、欠陥、コードの全内容を含む必要があります。
• 構成項目の正確なバージョンを記録する必要があります。
• 不具合の発生した状況を再現し、解決策を示す必要があります。
• ある時点での、ソフトウェアの状態を文書に記録して、認証監査時に準拠状況を証明します。

独立性

DO-178C/ED-12Cは、レベルAまたはBのソフトウェアのレビュー・アクティビティにおいて、独立性を重要視しています。独立性とは、ソフトウェア開発と検証アクティビティの客観性、正確性、徹底的な精査を明確にすることが基本原則です。さらに、レビュー対象となるソフトウェアライフサイクルデータ（software life cycle data）の開発者以外の担当者がレビューすることが独立性となります。ツールを使用することで、人による検証アクティビティと同等のレベルを達成することが可能です（DO-178C section6.2-e）。ソフトウェア・レベルAでは31項目中16項目（レベルBでは31項目中7項目、レベルC、Dでは該当なし）レビューobjectivesは、独立性を満たす必要があります。

レビューの独立性は、レビューのobjectivesを達成するために不可欠ですが、同時に、必要とされる工数に影響を及ぼす可能性があります：

– 人員の追加

– 必要な人員や専門知識を有する人員のスケジュール調整

– 文書化及びトレーサビリティの記録などの管理により全体的な経費の増加

レビュー・レコードの可用性

レビュー・レコードはコンプライアンスのエビデンスで、認証機関から要求されることがあります。したがって、データとデータベースが監査に使用できる場合、データベースからレビュー・レコードをエクスポートして成果物文書を作成する義務はありません。

文書の書式

文書の書式は、DO-178C/ED-12Cに準拠したレビューおよび解析の効率に影響を及ぼすことがあります。構造化された文書では、レビューは効率化され、レビューアーが要求事項への準拠を適正に審査できます。「文書が念入りに作成されていれば、長期間にわたって有用なものとなります。 反対に、広範にわたって活用されるのであれば、きちんと作成される価値があります。」A Rational Design Process: How and Why to Fake It、Parnas、Clements、1986

DO-178C/ED-12Cは、レイアウトや見栄えではなく、内容に重きが置かれています。そのため、文書は自由な書式や構成（例えば、データベース）をとることが可能です。レビューの工数を削減するために、「少ないほど良い（less-is-more）」ルールを適用し、詳細を必要なものだけに限定し、レビューアーが、全体像を把握できるようにして、適切に詳細を管理することが重要です。

最後に、ソフトウェア要求のレビューを自動化するために、自然言語処理（NLP）ツールで処理できる形式で表現可能な要求の記述ルールを定義する必要があります。

ソフトウェア・コンポーネントの定義

ソフトウェア・アーキテクチャとそのソースコードへの実装に関するDO-178C/ED-12Cレビューおよび解析のobjectivesは次の通りです：

• 6.3.3 b) このレビューobjectivesは、データフローおよび制御フローを介して、ソフトウェア・アーキテクチャのコンポーネント間の関係を検証することです。
• 6.3.4 b) このobjectivesは、ソースコードがソフトウェア・アーキテクチャで定義されたデータフローおよび制御フローと一致することを確認することです。

工数は、コンポーネントの定義、データフロー、コントロールフローの定義ならびに検証にツールを利用するかで大幅に異なります。DO-178C/ED-12Cでは、構成要素の規模や複雑さは、独立したソフトウェア・ モジュールまたは関数に始まり、サブシステム またはアプリ全体といった大規模なソフトウェア・ ユニットに至るまで、多岐にわたります。ここでは、DO-178C/ED-12CとDO-248C/ED-94Cに準拠したプロパティを紹介します：

• ソフトウェア・コンポーネントには、ソフトウェア・レベルが割り当てられます（DO-178C/ED-12C section2.3）。これは、ソフトウェア・コンポーネントがシステムの観点から可視化できることを意味しています。
• ソフトウェア製品（航空機搭載アプリケーションで使用されることを目的としたソフトウェア）は、複数のコンポーネントで構成されます（DO-178C/ED-12C section3.2）。
• ソフトウェア・コンポーネント間のインターフェイス（データフローおよび制御フローの形式）は、コンポーネント間で一貫性を保持するように定義する必要があります（DO-178C/ED-12C section5.2.2 d）。
• インターフェイスが下位のソフトウェア・レベルのコンポーネントに関連している場合、上位のソフトウェア・レベルのコンポーネントには、下位のソフトウェア・レベル・コンポーネントでの誤入力から保護するために、適切な保護メカニズムが備わっていることを確認する必要があります（DO-178C/ED-12C section6.3.3 b）。
• ソフトウェア・コンポーネントはサブプログラムとして定義することもできます（DO-248/ED-94C FAQ #67）。

したがって、ソフトウェア開発戦略に最も適したソフトウェア・コンポーネントの範囲を選択することが求められます。

リソースと時間の制約

プロジェクト管理に関する考慮事項はDO-178C/ED-12Cの範囲外ですが、時間や人員などのリソースが限られているため、レビューの範囲と深さが制限される可能性があります。重要なレビュー・アクティビティに優先順位を付け、品質を損なうことなくレビューがタイムリーに行われるよう、リソースを効果的に割り当てる必要があります。

この制約は、査読コメントが 「Status」、「Category 」または 「Severity 」のプロパティを含みます。

査読コメントを分類することが重要であるもう一つの理由は、EASAとFAAと連携して開発されたアドバイザリーサーキュラーadvisory circular（AC）であるAC 20-189 “Open Problem Reports (OPRs)” による未解決の問題報告書を管理することです。

次回

本稿では、DO-178C/ED-12Cのレビューおよび解析objectiveから得られる制約事項に焦点をあて、DO-178C/ED-12Cに準拠するために最低限のレビュー・フレームワークを記述する仕様書を書くための基礎を解説しました。次回は、DO-178C に準拠し、可能な限り効率的で最小限の実行可能なレビュー・フレームワークを定義する方法を解説します。

著者

———————————————————————————————————————————————————————————————————————–

• Olivier Appéré（オリヴィエ・アペレ）について

オリヴィエは認証エンジニアで、2022年にAdaCoreに入社しました。航空機ソフトウェアの認証分野で20年以上の経験を持ち、DO-178ソフトウェア安全認証規格に精通しています。AdaCoreでは、認証可能なアプリケーションに適したGNATランタイム・ライブラリを担当しています。

————————————————————————————————————————————————————————————————————————-

• Josue Bello（ジョスエ・ベロ）について

ジョスエは2022年よりAdaCoreの認証チームに所属しています。航空業界におけるソフトウェア、ハードウェア、飛行管理・誘導機能の認証に携わった経験を持っています。AdaCoreでは現在、ツール認定に従事し、ランタイム認証活動（ activities.）をサポートしています。

*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文こちらをご参照下さい。

 AdaCore クエンティン・オケム（Quentin Ochem） – 2024年9月27日

AdaCoreでは、組込システム向けの高信頼性ソフトウェアを開発するためのツールを提供しています。現在、プログラミング言語では、C/C++、Ada/SPARK、Rustをサポートしています。言語を選択する際に、「どうすればよいでしょうか? 最適なものは何ですか?」と質問されます。最良の答えを出すのは難しいですが、検討すべき項目を、解説します。

C/C++のリスク

組込では、C/C++が、一般的に「デフォルト」選択肢で利用されています。ソフトウェアの大部分は、すでにC/C++で記述され、多くの開発者は言語を理解し、ツールやプロセスも整っています。変更する必要はあるのでしょうか？

C/C++では、セーフティでかつセキュアなソフトウェアを開発には不向きな場合があります。長期にわたって研究と投資が行われてきましたが、費用対効果が高く、柔軟で信頼性の高い「セーフティなC/C++」はまだ存在していません。そのため、ほかの言語を選択することもできます。

開発プロセスを改善するRustとAda の使用

新たにプログラミング言語を検討する場合、現在2つの選択肢があり、それは AdaとRustです。どちらの言語も、C/C++と比較してセーフティとセキュリティの水準が高く、それぞれ独自の強みがあります。エコシステムとコミュニティに関して、Rust には、短期間で膨大な量のリソースを開発してきた活気のあるコミュニティが存在します。ただし、商用エコシステムはまだ組織化の過程にあり、AdaCoreはそれに貢献できる技術を備えています。そのギャップを埋めるには時間がかかります。対照的に、Ada のコミュニティは小さく、長年にわたってゆっくり成長しています。ただし、Ada には、ツールチェーンの可用性と認定ドキュメントの両方の面で、成熟したエコシステムが存在します。

さらに、言語機能に関して、Rust はメモリの安全性を高め、現在、存在するプログラミング言語よりも柔軟なメモリモデルを利用できます。Adaは、ソフトウェアとハードウェアの制約を定義し、検証できる優れた仕様言語です。つぎに、Ada と Rustの比較を表に示しますので、最適な言語を選択に利用してください。

SPARK – ソフトウェアの安全性を向上させる形式手法

C/C++以外の言語を選択する際に、SPARKはAdaやRustよりもさらに踏み込んだ選択肢となります。AdaをベースとするSPARKは、採用事例も多い強力な形式手法で、ソフトウェアがセーフティでセキュアであることを数学的に証明できます。ソフトウェア開発手法におけるこのパラダイムシフトは、高信頼性ソフトウェアに大幅なコスト削減をもたらします。

SPARKを使用すると、プログラム全体が形式化され、検証可能なプロパティを静的に、つまりコンパイル時に特定できます。AdaとRustには、Adaではハードウェア制約の指定、Rustではボローチェックによるメモリセーフティなど、静的にチェックされる基本的なプロパティがあります。SPARKはこのアプローチを極限まで高め、Adaの仕様言語を使用してプロパティを形式化し、自動的に証明します。

SPARKは、最初に脆弱性を検証します。例えば、配列要素へのアクセスに使われるインデックスが範囲内であるかを検証します。多くのプログラミング言語では、範囲外のアクセスは実行時に例外を発生しますが、SPARKは、範囲外のインデックスが存在する可能性がないことを静的に証明します。

SPARKは、任意プロパティに対して、コードが仕様に準拠しているかを検証できます。それは、シンプルなものから（ミューテックスに対する呼び出し元はバランスが取れていますか？　ソート呼び出しの後、配列は本当にソートされていますか？）から、関数の入力と出力の間のより複雑な関係などまでさまざまです。

最終的に、SPARKを使用することで、さまざまなチェックツール（例えばMISRA-Cチェックツール）の使用は不要となります。数学的証明によってプロパティを100％確実に検証することで、単体テストを省略可能です。これにより、直接的なコスト削減が実現され、全体的に高いレベルの整合性が確保されます。

最良の選択肢とは？

Ada、Rust、SPARKの選択は簡単ではありません。重要なのは、開発チームの目標を特定し、新しい変化を受け入れることが許容範囲なのかに依存します。以下の表は、選択する際に参考となる要素となります。なお、この見解はAdaCoreおよびAdaCoreのお客様が物事をどのように見ているかの指標です。

コミュニティ

Rustプログラミング言語の大きな強みの1つは、大規模で活気のあるコミュニティで、言語に関するリソースや、言語に情熱を持つ人々を簡単に見つけることができます。ツールやライブラリは、継続的にコミュニティで開発され、プロジェクトを始める際に簡単に利用することができます。

AdaおよびSPARKのコミュニティは比較的小規模です。AdaおよびSPARKを学ぶための優れたリソースは存在しますが、コミュニティ提供のツールやライブラリは多くはありません。しかし、長年にわたって試練を乗り越えて、献身的な人々によって構成され、新しいメンバーも増えつつあります。
全体として、両コミュニティは（活動の幅に差はありますが）潜在的な力から恩恵を受けています。それは、セーフティとセキュリティを求めるテクノロジーへの需要の高まりと言えます。

組込ツールチェーンのエコシステム

AdaとSPARKは、組込分野において、非常に成熟したエコシステムを持っています。LinuxやWindows環境以外にも、多くのリアルタイムOSやハードウェア・アーキテクチャ用のコンパイラが存在し、ツールは静的解析から動的解析まで、あらゆる要求に対応しています。また、ツールには長期サポートが提供され、1つのバージョンを選択すれば、何年、何十年とサポートを受け続けることができます。

今日のRustは、ネイティブ／サーバー環境で定着しつつあります。組込RTOSとアーキテクチャのサポートの多くは、開発中です。多くの環境をサポートする必要があるため、入手性、特殊性から、開発には長い時間がかかります。特定の環境はすでに市販されており、その他は（AdaCoreを含め）開発中で、長期的なサポートも重要です。プロバイダによっては、ツールチェーンを頻繁に更新する傾向があり、長期にわたるプロジェクトのサポートが困難になる可能性があります。AdaCore製品では、この問題に対応できます。

ツールチェーンに関しては、時間の経過とともに洗練されていきます。どちらの言語を選択するかの基準は、今日すべての答えを得ることが重要なのか、もしくは使用する側が待つことができるのか、ということとなります。

安全認証

認証の状況は、ツールチェーンのサポートの状況と同様です。AdaとSPARKは、すでに多くの実績があり、特に組込の世界で最も一般的な規格である航空電子機器（DO-178）、自動車（ISO 26262）、鉄道（EN-50128）、宇宙（ECSS-E-ST-40C、ECSS-Q-ST-80C）など、幅広い規格の認定と認証のエビデンスを持っています。

Rustはかなり歴史の浅い技術であるため、認定を受けるまでにはまだ時間がかかります。自動車のISO-26262のエビデンスが出始めていますが、これは現在、一部の環境とRustツールチェーンの一部のサブセットに限られています。

ライブラリ

Rustプログラミング言語の特長のひとつは、カーゴ・パッケージ・マネージャから利用できる多くのライブラリがあることです。考えられるほとんどのものが、用意されています。しかし、このライブラリの多くは趣味で開発されており、最も人気のあるライブラリの多くはまだバージョン1.0です。

AdaとSPARKは、既製ライブラリの数は多くありません。2021年に開始されたAlireパッケージ・マネージャは、現在、数百のパッケージを提供しています。また、ネイティブ・ライブラリは多くはないですが、AdaとSPARKから既存のCまたはC++ライブラリへのバインディングによって対応しています。

しかし、どちらの言語についても、規制または認証要件から制約が生じる可能性があります。一般的に公開されているライブラリは、セーフティまたはセキュリティ認証を取得している組込開発には適していないからです。

プログラミング思想

プログラミング思想に関して、Ada、SPARK、Rust の間には根本的な違いはありません。いずれも命令型モジュール言語であり、オブジェクト指向の概念や類似した機能が用意されています (関数型言語などとは対照的です)。すべて静的にマシンコードに直接コンパイルされます (インタプリタ型言語などとは対照的です)。

プログラミング・エラーの回避

３つの言語はすべて、プログラミング・エラーを回避または軽減するためのメカニズムを備えています。たとえば、3つの言語は、境界を含み、動的なインデックスチェックを可能にする配列を第一級オブジェクトとして扱っています。また、初期化されていない変数、データ競合、ヌルポインタの逆参照などを回避するためのさまざまな方法も用意されています。

強い型付け

強い型付けにより、コンパイル時にオブジェクトの特定の型を決定し、その値の整合性をチェックできます。C は、弱い型付けで、変数は型付けされますが、暗黙的な変換により、暗黙のうちに異なる表現の数値を混在させることができます (たとえば、整数と浮動小数点数を追加する場合)。そのため、オーバーフロー、アンダーフロー、丸めエラーなどの問題が発生する可能性があります。配列をポインタのように扱うことは、弱い型付けから生じる問題のもう一つの例です。Rust の型付けはより強力で、明示的な変換なしで異なる型を混在できず、配列は第一級オブジェクトです。そのため、一般的なプログラミングミスを回避できます。

Ada と SPARK はさらに進化しています。型はソフトウェア設計の基本要素になります。型には名前が付けられ、プロパティに関連付けされ、静的および動的に一貫性がチェックされます。たとえば、ある浮動小数点をマイル単位の距離として宣言し、別の浮動小数点をパーセンテージとして宣言すると、明示的な変換を行わなくても、誤って混同するリスクがなくなります。同様に、緯度と経度の浮動小数点型を定義して、型システムによってサブプログラム呼び出しや演算でそれらが混同されることを防止できます。強力な型付けにより、コーディングエラーだけでなく設計の不一致も検出できます。

データ制約、ハードウェア/ソフトウェアデータの一貫性

Ada および SPARK 型では、データ範囲、表現制約条件、妥当性述語などのさまざまなプロパティを型に関連付けることができます。たとえば、パーセンテージ型は 0 ～ 100 、緯度は -90 ～ 90 度に制約できます、経度は -180 ～ 180 度に制約できます。この制約は、静的および動的検証可能です。データ構造は、特定のエンディアンを使用してメモリ内のビットレベルで指定できるため、ビット単位の演算に関連する間違いを回避できます。仕様表現の一貫性は静的にチェックされます (たとえば、構造のフィールド間に重複がないこと、型一致に指定されたビット数が取り得る値に対して十分であること、浮動小数点値の精度をハードウェアで実装できることなど)。

Rustはこの機能を備えていないため、必要に応じて、適切に定義された構造体などを使用して、従来の設計方法で対応することができます。

ランタイム・エラーがないことの保証

ランタイム・エラーとは、プログラムの実行中にチェックやアサーションによって検出できるエラーを指します。例えば、配列要素へのアクセスに使用されるインデックスが有効かどうかを検証します。AdaとRustは、データの有効性を検証するランタイム・チェックを提供しており、失敗した場合は例外を発生させるか、パニックを発生させます。これらの機能は、コード・サイズやパフォーマンスにおいて小さなフットプリントのため、バッファ・オーバーフローのような脆弱性からコードを保護することができます。SPARK は、コンパイル時に実行時エラーがないことを証明します。たとえば、SPARK は、値を範囲外に置く可能性のあるコードがないことを静的にチェックできます。そのため、パフォーマンスの低下を回避できるだけでなく、潜在的な例外/パニックに対してコードが適切に実行できる利点があります。ただし、追加の制約、アサーション、および契約（Contract）を表現する作業が増えます (後のセクションを参照してください)。

契約（Contract）言語（事前事後条件（pre- post- conditions）、不変条件（invariants）、述語（predicates）

AdaとSPARKは、ソフトウェア・エンティティ、特に型と関数に関する契約（Contract）を記述できるという点で 特徴的です。そのため、制約条件や 動的な動作の期待値を仕様の一部としてエンコードし、アプリケーション全体で妥当性をチェックすることができます。

Ada は、この契約（Contract）を、実行時に検証される動的チェックに変換します。これは、コードのサイズとパフォーマンスに影響がありますが、テスト、デバッグ、統合の段階で有用で、コンパイル時に取り除くことができます（すべて、または部分的に）。契約（Contract）のエラーは通常、例外に置き換えられます。

SPARKでは、契約（Contract）がアプリケーションが満足することを形式的、数学的に証明することができ、どのような値が操作されたかにかかわらず、指定された制約条件と機能要件が満足することが保証されます。この場合、契約（Contract）をコンパイルして動的なチェックを行う必要がないため、容量やパフォーマンスのペナルティが生じません。そのためSPARKはプログラミングの矛盾を解決する手段を提供するため検証を重視できます。

現在、Rustにはこの機能を実装できる仕様はありません。動的チェックを目的とした防御コードやアサーションによって、ある程度実現することは可能です。しかし、SPARKのように、プロパティを形式的に証明できる機能は、Rustには、今のところありません。

メモリの安全性

Rustの強力な機能の1つは、メモリの所有権モデルを通じてメモリエラーを回避できる点です。そのため、ソフトウェアにおける重大なセキュリティ脆弱性の原因を排除できます。Rustを採用し、所有権モデルに従い、ボローチェッカを満たすことで、メモリエラーを避けることができます。

最新のAda（2022年）は、ポインタ回避方法を提供し、メモリ破損のリスクを軽減します。しかし、特定のプログラミンムではポインタの使用が必要であり、明示的な所有権モデルやボローチェッカがない場合、メモリの問題が発生する可能性があります。

一方、SPARKは強力な所有権モデルとボローチェッカを追加し、Rustと同じレベルの保証を提供可能です。

導入コスト

AdaとRustの導入コストは同等です。どちらの場合も、新しい言語を習得して、ツールチェーンを導入する必要があります。影響は軽微とは言えませんが、全体的なプログラミングプロセスは殆どそのままで済みます。

SPARK採用に必要なコストは、多分それ以上かかると思われます。最初のAdaとツールチェーンと言語に関する検討事項はほぼ同じです。しかし、実際にSPARKを採用することは、異なるプログラミング方法を採用することを意味しています。効果的であるためには、形式検証を開発プロセスに統合し、ソフトウェアの設計方法を変更する必要があります。これは決して単純な決定ではなく、想定されるコスト削減効果に応じて、証明すべきプロパティを優先することもあれば、優先しないこともあります。ただし、その結果得られるメリットは極めて大きくなります。

メリット

メリットはプログラムに依存し、高信頼性開発の観点から言語を見ています。

大まかな視点では、AdaやRustを採用するメリットはよく似ています。どちらの言語もプログラミング・エラーの確率を大幅に軽減します。方法は異なりますが、どちらの言語もメモリセーフティに対応しています。Rustのメモリモデルを利用すると、現在のAdaのポインタ回避方法よりも進化していますが、Adaの強力な仕様と型付けによって、Rustには実現できない一貫性チェックが可能になります。 Adaに関する論文では、C言語と比較して、最大40%の開発コスト削減可能であることが説明されています。これには、製品に含まれる可能性が低いバグの削減は考慮されていません。

SPARKは強力な形式手法を提供し、AdaやRustの利点をはるかに凌ぐ可能性があります。開発の初期段階で多くの検証が行われるため、後段のテストやチェックは省略することが可能です。それは、SPARKで表現された制約条件や特性をチェックするような検証です。特定された動作に対する障害は、緩和されるのではなく、除外されます。不具合の代償が大きい耐用年数が長期にわたるアプリケーションの場合、言語を変更することによって大きな利益をもたらす可能性があります。

その他のブログ： #Ada    #Rust    #SPARK    

クエンティン・オケム（Quentin Ochem）はAdaCoreのチーフプロダクト＆レベニューオフィサーで、マーケティング、セールス、プロダクトマネジメントを統括しています。AdaCoreとの関わりは学生時代の2002年に始まり、2005年に正式に入社し、IDEとクロス言語バインディングに携わってきました。ソフトウェアエンジニアリング、中でも航空電子工学や防衛などの高信頼性領域でのバックグラウンドを有しています。その後、トレーニングやテクニカルセールスを担当するようになり、テクニカルセールス部門の立ち上げや米国でのグローバル製品管理にも携わるようになりました。2021年に現在の職務に就任し、AdaCoreの戦略的取り組みを主導しています。

2005年にマルセイユ工科大学でコンピューター工学の修士号を取得しています。

*本資料は、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およびその関連サプリメントの開発にも携わりました。

DO-178についてもっと知る »

認定ツール、ランタイムライブラリ、および認定資料

AdaCoreのいくつかのツールは認定を受けており、コーディング標準への準拠、バッファオーバーランや整数オーバーフローなどのエラー防止、MC/DC（修飾条件/決定条件）の構造カバレッジ解析など、検証目標を達成する際の労力を軽減します。

さらに、Ravenscarタスクプロファイルを実装した高保証ランタイムライブラリは、認定システムに組み込むのに十分シンプルである一方、ハードリアルタイムのアビオニクスソフトウェアに求められる機能をサポートします。これらのツールとライブラリには認定資料も用意されており、新しいプロジェクトにも柔軟に適用可能です。

サステインド・ブランチ（Sustained Branch）サービス

認定ソフトウェアの保守には、特定のバージョンを「固定（フリーズ）」する必要があり、安定性を維持するための独自の課題が伴います。しかし、ソフトウェアの進化に伴い問題が発生した場合には、更新されたリリースが必要となる場合もあります。

AdaCoreの「サステインド・ブランチ」サービスは、このような課題に対応するために提供されており、DO-178B / DO-178Cのガイダンスに沿った形でこの要件をサポートしています。このサービスは、GNAT Pro保証製品の標準的な一部として提供されています。

————————————————————————————————————————————————————————————————————————–

AdaCoreは、DO-178B/C認証のコスト削減やワークフローの効率化を支援するさまざまなツールとサービスを提供しています。その中心となるのが、重要なシステム向けに特化したAda開発環境「GNAT Pro Assurance」です。

————————————————————————————————————————————————————————————————————————–

• GNAT Pro Assurance

GNAT Pro Assuranceには、「サステインド・ブランチ」と呼ばれる専門サービスが含まれており、プロジェクトで使用する特定の技術バージョンを安定的に維持しつつ、重要な問題を修正するためのアップグレードが可能です。この環境は、Ada言語の全バージョンをサポートし、オプションでC言語サポートも追加できます。

さらに、GNAT Pro Assuranceには完全なツールスイートが含まれており、構成可能なランタイムライブラリや、高保証システムに特に適した専用ランタイムライブラリも提供されています。

•  SPARK Pro

SPARK Proは、安全性やセキュリティが最優先されるアプリケーションの開発に特化した言語およびツールセットです。このツールセットは、高い信頼性、低い誤警報率、深い静的検証を実現し、安全性やセキュリティに関する認証要件を満たすための正確な証拠を生成します。

• GNAT Static Analysis Suite

GNAT SASは、開発者がコードを深く理解し、信頼性が高く安全なソフトウェアを構築するための支援を行うAdaソースコードアナライザーです。このツールは、ランタイムエラーやロジックエラーを検出し、プログラム実行前に潜在的なバグや脆弱性を評価します。

GNAT SASは、自動化されたピアレビュー機能としても機能し、開発ライフサイクルのどの段階でもエラーを容易に発見できます。これにより、コードの品質向上や安全性・セキュリティの分析が効率化されます。

• GNAT Coverage

GNAT Coverageは、オブジェクトコード（命令および分岐カバレッジ）とAdaやC言語のソースコード（ステートメント、決定、修飾条件/決定カバレッジ – MC/DC）の両方についてカバレッジ分析を行います。これにより、ソフトウェアの動作やテストの完全性を詳細に評価できます。

DO-178C / ED-12CとAdaCoreの技術

DO-178C / ED-12C規格のガイダンスと、技術固有の補足資料は、航空機搭載ソフトウェアがその要件を満たしていることを証明するための重要な指針を提供します。このガイダンスへの準拠を証明することは特に検証活動において困難を伴いますが、認定ツールや専用ランタイムライブラリを適切に活用することで、作業を大幅に効率化することが可能です。

本資料では、AdaCoreが提供する各種テクノロジー（ツール、ライブラリ、補足サービス）が、このプロセスをどのように支援できるかを解説します。

ダウンロード【英語版】

*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文こちらをご参照下さい。

2023/11/9

AdaCore、Rust コンパイラで初の認定を取得したことを発表しました。

TÜV SÜDは、RustコンパイラにISO 26262認定証を世界で初めて交付しました。

AdaCore（ソフトウェア開発ならびに検証ツールプロバイダ） は本日、ISO 26262 の最上位のレベルであるASIL Dが必要なソフトウェアの開発に使用できるRust コンパイラで初めての認定証を TÜV SÜD が発行したことを発表しました。

認定取得に際して、AdaCoreは強力なサポートを提供し、年初に締結されたパートナーシップの一環として実現されました。

AdaCoreは、ツールチェーンの認定に関して豊富な経験を有しており、今回のRustコンパイラで、17回目のツールチェーンの認定を取得したことになります。AdaCoreの認定と認証に関する長年の経験により、初期段階から最適な手法を用いて、認定期間を短縮できました。

「今回のRustコンパイラの認定は、2年以上にわたる努力が実りました。」と、AdaCore GNAT Pro for Rustの Technical Lead　Hristian Kirtchevは語っています。

「このRustコンパイラは、アップストリームコミュニティによって開発されたrustcのバージョン1.68に基づいています。認定取得のために、まずRustプログラミング言語でサポートされるサブセットを特定して、次にサポートされる言語機能の厳密な仕様を策定しました。さらに、アップストリームテストを仕様に照らし合わせ、必要に応じてテストを作成し、最後にエンドユーザーが選択したコンパイラスイッチを用いて、特定のプラットフォームをターゲットとするコンパイラのテストを実施しました。その結果、認証済のアプリケーションで、コンパイラが正しいコードを生成することが確認できました。」

AdaCoreは、この認証プロジェクトの成功を受けて、GNAT Pro for Rustを認証取得するセーフティ・クリティカルならびにセキュリティ・クリティカル・アプリケーションに適用することを目指しています。

「認証取得時に使用するプログラミング言語では、認定済ツールチェーン、認証済ランタイム・ライブラリ、認定済サポート・ツールの3つが必要です。」と、AdaCoreのGNAT Pro for RustのProduct Manager Tony Aielloは語っています。

「ツールチェーンが認定されることは、顧客が認証を取得するための第一歩です。GNAT Pro for Rustは、Rustを認証に使用するためのソリューションを提供します。」

AdaCoreは、顧客がRustの豊富な言語機能を最大限に活用するために、Rustのランタイム・ライブラリによるサポートを重要と考えています。さらに、認証基準では、コードカバレッジやコーディングスタンダードの準拠の証明、ならびに認定ツールのサポートが必要となる付加的な活動が必須となります。

GNAT Pro for Rustは、認証済ランタイム・ライブラリならびに認定済サポート・ツールを含んだツールチェーン一式をお客様に提供するために、この認定から学習した内容を基に構築されています。

GNAT Pro for Rustの詳細については、今すぐお問い合わせください！

AdaCoreについて

1994年に設立されたAdaCoreは、ミッション・クリティカル、セーフティ・クリティカル、かつセキュリティ・クリティカルなシステム向けにソフトウェア開発・検証ツールを提供しています。

長年にわたり、AdaCore製品を利用されているお客様は、セーフティ・クリティカルなアプリケーションを開発し、保守を継続されています。その分野は、商用航空機、自動車、鉄道、宇宙、軍事、航空交通管制、医療機器、財務サービスなどです。AdaCore社の顧客は、世界的に幅広い分野で増え続けています。詳細については、こちら（英語）をご覧ください。

AdaCore製品はオープンソースで、開発エンジニア自身が専門的なオンラインサポートを提供しています。同社の拠点は、ニューヨークならびにパリにあります。AdaCoreホームページ

※本資料は、AdaCoreのプレスリリースを意訳したものです。正確な内容については、原文こちらをご参照下さい。

RTCA DO-178C / EUROCAE ED-12Cは、航空機搭載システム向けソフトウェア認証に関するDO-178B/ED-12B規格の改訂版です。
「コア」ガイダンスの改訂は一部で、４つの新しい文書が追加されました。:

• Software Tool Qualification Considerations (RTCA DO-330 / EUROCAE ED-215)
• 特定の開発手法のための 「サプリメント」
  • Model-Based Development and Verification (RTCA DO-331 / EUROCAE ED-218)
  • Object-Oriented Technology and Related Techniques (RTCA DO-332 / EUROCAE ED-217)
  • Formal Methods (RTCA DO-333 / EUROCAE ED-216)

2011年12月に公開された規格は、「耐空性要件に適合する安全性の信頼レベル( a level in confidence in safety that complies with airworthiness requirements )」を達成するオブジェクトに基づいたアプローチ( objectives-based approach )を規定する当初のDO-178Bの主旨を保持し、1990年代初頭にDO-178Bが公開された以降の技術的進歩を考慮にいれ、ガイダンスを改訂しています。

DO-178Bの変更点

改訂作業は2004年末にRTCA特別委員会#205（SC-205）とEUROCAE作業部会#71（WG-71）の合同委員会で始まり、主な目的は以下の通りです：

• DO-178Bのエラーを修正し、紛らわしい内容を明確にする
• DO-178Bの発行以降に成熟し、実用化されたソフトウェア技術とスタンダードに対応する
• DO-178B をサポートする補足資料 (Certification Authorities Software Team (CAST) の文書や問題に関する文書 (IP) など) を考慮する

当初は、セーフティケース解析を必須にして、「プロセス 」ベースから 「製品 」ベースに文書の性質を変更することが議論されましたが、必要最小限の変更にとどめ、DO-178Bと比較して認証の難易度の変更が最小になるように合意されました。DO-178B規格は機能しており、大幅な方向転換は不要であり、適切でないと判断されました。

「コア・ガイダンス」の変更は比較的軽微です。詳細な議論は、フレデリック・ポトン（Frédéric Pothon）の論文「DO-178C/ED-12C versus DO-178B/ED-12B: Changes and Improvements << http://www.adacore.com/uploads/technical-papers/DO178C-ED12C-Changes_and_Improvements-Sep2012.pdf>>」に記載されています。

更新の内容は以下となります。

• システムとソフトウェアのライフサイクルプロセス間の情報フローの処理範囲の拡張
• オブジェクト・コードがソース・コードにトレースできない場合のレベルAの新しい検証オブジェクティブ（verification objective）
• 強力に連結された条件を扱うことができる新しく導入されたマスキング MC/DC

ツール資格

DO-178Cの新しいドキュメントとしてSoftware Tool Qualification Considerations(DO-330/ED-215)があります。これは分野に依存せず、DO-178C以外の高信頼性規格と併用できるため、厳密には補足ではありません。DO-178Bの検証ツールと開発ツールの概念は、3つのツール資格認定基準に置き換えられています：

Criterion 2 は新しく、ソース コードのレビューに静的解析ツールを使用し (たとえば、再帰がないことを実証する)、その結果を使用してコンパイル済みコード内のスタック チェックの削除を正当化するなどの状況に対応します。
DO-178Cは、ソフトウェアレベルとツールCriterionに基づいて、5つのツール資格レベル(TQL)を定義しています。

DO-330 は、DO-178C と同じ構造を使用して、各TQL の特定のガイダンスを定義しています。ツール・ユーザは、ツール開発者から提供された資料 (特に、操作環境、機能動作、その他の内容を文書化したツール運用要件) を含む、資格認定成果物を用意する必要があります。TQL-1からTQL-4までの資格認定活動は、レベルAからDまでの認証活動とほぼ同等で、TQL-5は、DO-178Bの検証ツールに相当します。

テクノロジーサプリメント

1992年にDO-178Bが発表されて以来、多くのソフトウェアエンジニアリング方法論が成熟し、航空機搭載システムの開発者には有益でした(また、問題も提起しています)。DO-178Cの取り組みでは、3つの技術の問題点を分析して、必要に応じてDO-178Cのガイダンスを適応し、拡張するサプリメントを用意しました。このサプリメントでは、検証プロセスに焦点を当てています。

• Model-Based Development and Verification (RTCA DO-331 / EUROCAE ED-218)

モデルベース開発では、システム要件、設計アーキテクチャ、および動作は、正確な(通常はグラフィカルな)モデリング言語で指定され、コードを自動的に生成するツールで処理され、場合によってはテストケースも生成されます。認定済モデリングツールを使用すると、ライフサイクルの短縮/簡素化、要件の正確な(そして理解しやすい)仕様など、多くの利点があります。しかし、モデルベース開発では、システムとソフトウェアのライフサイクルプロセスの統合、複雑なトレーサビリティ、モデルベース開発の観点でのカバレッジ解析の意義など、多くの課題も生じます。DO-331 のガイダンスでは、この問題に対処しています。

• Object-Oriented Technology and Related Techniques (RTCA DO-332 / EUROCAE ED-217)

オブジェクト指向 (システムのアーキテクチャが、システムが扱うエンティティの種類とその関係に基づく設計アプローチ) は、新しい要件を満たす必要がある場合にシステムを拡張するタスクを容易にできるため、数十年にわたってソフトウェア開発の主力となっています。しかし、オブジェクト指向テクノロジ (OOT) で、表現力を高めるプログラミング機能 (継承、ポリモーフィズム、動的バインディング) は、多くの重要な技術的問題を含んでいます。つまりOOTのダイナミックフレキシビリティは、プログラムプロパティを静的に検証するDO-178BおよびDO-178C要件と矛盾するため、DO-332 のガイダンスでは、この問題に対処しています。それは、型置換可能性に新たな検証Objectiveを導入し、型特殊化のみに継承が利用されます。

• Formal Methods (RTCA DO-333 / EUROCAE ED-216)

証明技術とハードウェア速度の進歩に伴い、ソフトウェア検証における形式（数学的な）手法の使用は、セーフティ/セキュリティ・クリティカルの高いレベルでは、広範な分野で使用されています。形式手法は、実行時エラーが発生しないことや、モジュールの実装が形式要件に準拠していることまで、プログラムのプロパティを証明するために使用されています。

DO-178Bでは、コンプライアンスの代替手段として形式手法が規定されましたが、他のObjectiveへの適合についての共通理解はありませんでした。DO-333では、この点を考慮して、形式手法が他の検証活動、特に特定の要件ベーステストを補完または置き換える方法を提供します。

その他の資料等

• L. Rierson. Developing Safety-Critical Software: A Practical Guide for Aviation Software and DO-178C Compliance. CRC Press, 2013
• F. Pothon. DO-178C/ED-12C versus DO-178B/ED-12B: Changes and Improvements.
  www.adacore.com/uploads/technical-papers/DO178C-ED12C-Changes_and_Improvements-Sep2012.pdf

• AdaCore. High-Integrity Object-Oriented Programming in Ada; June 2013.
  extranet.eu.adacore.com/articles/HighIntegrityAda.pdf

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

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

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

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

*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文こちらをご参照下さい。

ED-203A / DO-356A セキュリティ反証（Refutation）オブジェクティブに関するガイドラインと考慮事項

このレポートは、2つの技術的に同一の文書に記載されているセキュリティ反証（Refutation）に関して、ガイドラインと考察を提供します。
ED-203A ED-202A プロセス仕様と ED-203A の手法と考慮事項 「Airworthiness Security Methods and Considerations」, European Organization for Civil Aviation Equipment (EUROCAE)
DO-356A 耐空性セキュリティ手法と考慮事項「Airworthiness Security Methods and Considerations」, Radio Technical Commission for Aeronautics (RTCA)

ED-203A/DO-356Aでは以下のように記述されています。

「反証（Refutation）は、解析や要件を超えた独立した保証手段（assurance activities）として機能します。徹底的なテストに代わるものとして、反証（Refutation）は、許容可能な範囲で、予期しない振る舞いが抑止されているという証拠を提示するために使用可能です。注: 反証（Refutation）は、状況によってはセキュリティ評価とも呼ばれます。」 [ED-203A / DO-356Aから引用）。

このレポートでは、反証活動が関連する耐空性セキュリティプロセスにどのように適合するかを要約しています。さらに、認証のセキュリティに関する計画（PSecAC）に反証（Refutation）試験計画を含めるためのガイドラインと考慮事項を示しています。そして、特定の反証（Refutation）活動に関する追加ガイドラインを対象とした、附属文書が提供されています。また、附属文書Aでは「ファズテスト」を取り上げています。

[日本語版]　ダウンロード

[原文　英語版]　ダウンロード

AdaCoreについて

1994年に設立されたAdaCoreは、ミッション・クリティカル、セーフティ・クリティカル、かつセキュリティ・クリティカルなシステム向けにソフトウェア開発・検証ツールを提供しています。

長年にわたり、AdaCore製品を利用されているお客様は、セーフティ・クリティカルなアプリケーションを開発し、保守を継続されています。その分野は、商用航空機、自動車、鉄道、宇宙、軍事、航空交通管制、医療機器、財務サービスなどです。AdaCore社の顧客は、世界的に幅広い分野で増え続けています。詳細については、こちら（英語）をご覧ください。

AdaCore製品はオープンソースで、開発エンジニア自身が専門的なオンラインサポートを提供しています。同社の拠点は、ニューヨークならびにパリにあります。AdaCoreホームページ

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

2024年10月吉日

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

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

記

開催概要

「出展の見どころ」

• 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 を使用します。