知識マップ: GigE VisionのパケットをAdaの型で受ける ── 表現句の落とし穴とSPARKで証明するパーサー

記事「GigE VisionのパケットをAdaの型で受ける ── 表現句の落とし穴とSPARKで証明するパーサー」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

GigE Visionのカメラは画像をGVSPのパケットで送る。Adaのレコードの表現句でヘッダーを型にするとき、ビット番号の数え方はBit_Orderで決まり、リトルエンディアンのCPUでビッグエンディアンの整数を読むにはGNAT独自のScalar_Storage_Orderも要る。Unchecked_Conversionで作った値は使う前にValid属性で確かめる。長さを確かめてから1フィールドずつ読み出すパーサーは、範囲外を読まないことと読み出す関数の事前条件をGNATproveで証明できる。

flowchart LR
    accTitle: GigE VisionのパケットをAdaの型で受ける記事の知識マップ
    accDescr: GigE VisionがGVSPで画像を送り、GVSPのヘッダーをWiresharkで確かめられること、レコードの表現句のビット番号はBit_Orderで決まり、バイト順にはScalar_Storage_Orderが要ること、Unchecked_Conversionで作った値はValid属性で確かめること、範囲外を読まないことと事前条件をGNATproveで証明することを示す図。
    gvsp["GVSP"]
    ada_record_representation_clause["レコードの表現句(record representation clause)"]
    spark_silver_level["Silverレベル(AoRTE)"]
    gige_vision["GigE Vision"]
    wireshark["Wireshark"]
    ada_bit_order["Bit_Order"]
    gnat_scalar_storage_order["Scalar_Storage_Order"]
    ada_unchecked_conversion["Ada.Unchecked_Conversion"]
    ada_valid_attribute["'Valid属性"]
    gnatprove["GNATprove"]
    design_by_contract["契約による設計(Pre/Post)"]
    gige_vision -->|"利用する"| gvsp
    gvsp -->|"で確認できる"| wireshark
    ada_record_representation_clause -->|"で構成できる"| ada_bit_order
    ada_record_representation_clause -.->|"前提とする"| gnat_scalar_storage_order
    ada_unchecked_conversion -->|"で確認できる"| ada_valid_attribute
    spark_silver_level -->|"で確認できる"| gnatprove
    design_by_contract -->|"で確認できる"| gnatprove

概念間の関係(全7件)

図と同じ関係を文章でも列挙します。表示している文と機械可読な意味データ(RDFa)は同じ要素に載っています。確度が「確立した関係」のものは直接の関係として、「条件付きの関係」のものは成立条件つきの言明(rdf:Statement)として表現しています。

GigE VisionはGVSPを利用します。GigE Visionのカメラは、撮った画像をGVSPでUDPのパケットに分けて送る。1枚の画像はleader、payload、trailerのパケットになる / 確度: 確立した関係 / 確認日: 2026-11-10 出典出典
GVSPはWiresharkで確認できます。WiresharkにはGVSPの解析部があり、標準IDと拡張IDのヘッダー、画像のleaderとtrailerのフィールドを読める。記事はフィールドの配置をこの解析部のソースとAravisの定義で確かめた / 確度: 確立した関係 / 確認日: 2026-11-10 出典出典
レコードの表現句(record representation clause)はBit_Orderで構成できます。表現句のビットの位置をどちらの端から数えるかはBit_Orderで決まる。High_Order_Firstにすると0番が最上位のビットになり、ネットワークのヘッダーの図と同じ数え方で書ける / 確度: 確立した関係 / 確認日: 2026-11-10 出典
レコードの表現句(record representation clause)はScalar_Storage_Orderを前提とします。Bit_Orderは複数バイトの整数のバイト順を変えないので、リトルエンディアンのCPUでビッグエンディアンのヘッダーを表現句の型で読むには、GNAT独自のScalar_Storage_Orderも指定する。記事の例ではx86-64でBit_Orderだけの型が42を10752と読んだ / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典出典
Ada.Unchecked_Conversionは'Valid属性で確認できます。Unchecked_Conversionの結果は型の値を表すとは限らず、使い方によっては実行がerroneousになる。列挙型などの成分は使う前にValid属性で確かめる。記事の例では形式のバイトが0x09のヘッダーでFormat'Validが偽になった / 確度: 確立した関係 / 確認日: 2026-11-10 出典出典
Silverレベル(AoRTE)はGNATproveで確認できます。SPARK_Modeのパーサーについて、配列の範囲外を読まないこと、整数があふれないこと、列挙型への変換が範囲を外れないことを、すべての入力についてGNATproveで証明する。フィールドの位置が仕様どおりかは証明の対象ではない / 確度: 確立した関係 / 確認日: 2026-11-10 出典出典
契約による設計(Pre/Post)はGNATproveで確認できます。バイト列から読み出す関数の事前条件が呼び出しのたびに成り立つかを、GNATproveが手前の長さの確認から確かめる。長さの確認が漏れた呼び出しは、事前条件が成り立たない可能性として報告される / 確度: 確立した関係 / 確認日: 2026-11-10 出典

主要概念の定義

GVSP: GigE Visionでカメラが画像を送るのに使うUDP上のプロトコル。1枚の画像をleader・payload・trailerのパケットに分けて送り、各パケットは状態コードとブロックID・パケットIDを持つヘッダーで始まる。
レコードの表現句(record representation clause): Adaで、レコードの各成分をレコードの先頭から何バイト目の何ビット目に置くかを指定する表現項目。
Silverレベル(AoRTE): 範囲外アクセス・オーバーフロー・ゼロ除算などの実行時エラーが起きないことを証明する、証明レベルのうち実務上の既定目標とされる段階である。
GigE Vision: Ethernetでカメラの制御と画像の送信を行うマシンビジョン向けのインターフェース規格。制御にGVCP、画像の送信にGVSPというUDP上のプロトコルを使う。
Ada.Unchecked_Conversion: ある型のビット列を、検査せずに別の型の値として解釈し直すAdaの総称関数。結果が変換先の型の値を表すとは限らない。
契約による設計(Pre/Post): サブプログラムの入口での前提条件(Pre)と、出口で保証する性質(Post)を宣言的に記述する、Ada 2012の契約機構である。

機械可読データ

JSON-LD / Turtle ── この記事の知識グラフ全体
概念一覧 / 語彙(述語)の定義

このデータセットについて

作成: 合同会社小村ソフト
ライセンス: CC BY 4.0 ── 出典(合同会社小村ソフト)とライセンスへのリンクを明示し、改変した場合はその旨を示すことを条件に、再配布・改変を含めて再利用できます
最終確認日: 2026-11-10 ── 収録する関係のうち、最後に出典と照合した日

このページはサイトの知識グラフ(_data/knowledge/)から自動生成されています。誤りの指摘はお問い合わせからお願いします。