ESBMC-Arduino: オープンハードウェアPLCの形式検証におけるデプロイメントギャップを埋める

コンピュータサイエンス > プログラミング言語 arXiv:2607.08550 (cs) [2026年7月9日提出] タイトル: ESBMC-Arduino: オープンハードウェアPLCの形式検証におけるデプロイメントギャップを埋める著者: Pierre Dantas, Lucas Cordeiro, Waldir Junior タイトル「ESBMC-Arduino: オープンハードウェアPLCの形式検証におけるデプロイメントギャップを埋める」のPDFを表示、Pierre Dantasと他の2名の著者によるPDF HTML（実験的）を表示 概要: OpenPLC、Arduino OPTA、CONTROLLINO、Industrial Shields M-Duinoは、実際の自動化および産業制御システム（ICS）セキュリティ研究で使用される低コストマイクロコントローラーにIEC 61131-3をもたらします。ESBMC-PLCを含む、IEC 61131-3用の既存のオープンソース検証ツールは、抽象的なスキャンサイクルモデルと理想的な無限整数を使用して安全性を証明します。ボードアーティファクトは、16ビットワード（8ビットAVR Arduino）を持つリソース制約のあるマイクロコントローラーユニット（MCU）で実行され、センサーは有限解像度のアナログ・デジタル・コンバーター（ADC）を介して読み取られます。このデプロイメントギャップにより、幅を意識した単純な検証は健全性を欠くことがわかります。123の実際のプログラムのうち、ハードウェア入力モデルなしで16ビットオーバーフローをチェックすると、44%の誤警報（54/123）が発生し、ADCでは生成できないセンサー値を探索するため、実際の欠陥は見つかりません。ギャップは計算が物理プロセスと出会う場所、つまり有限幅の算術演算によってスケーリングされた有限解像度のセンサー値がアクチュエーションコマンドに変換される場所にあり、オーバーフローは高レベルアラームなどの安全アクションを静かに抑制する可能性があります。無限入力モデルは、環境がトリガーできないアラームを捏造します。オープンハードウェア上のIEC 61131-3のハードウェア忠実な検証を提案します。宣言的なハードウェア抽象化レイヤー（HAL）記述子（幅、ADC/PWM解像度、I/Oバインディング）と、ターゲット幅で算術演算を解釈し、ハードウェアで実現可能な範囲に入力値を制約するサウンドなローリングです。Arduino用にこれをインスタンス化し、ArduinoToolとして、公式コアからHALパラメータを導出し、ESBMCラダーダイアグラム（LD）フロントエンドで入力範囲モデルを実現します。123プログラムのコーパスでは、HALアノテーターは54の誤警報をすべて排除しつつ、堅牢性証明を維持し、制御されたコーパスは、実現可能な証拠とともに検出するまれな幅依存の欠陥を示します。コメント: 21ページ 件名: プログラミング言語 (cs.PL); ハードウェアアーキテクチャ (cs.AR); システムと制御 (eess.SY) 引用形式: arXiv:2607.08550 [cs.PL] (またはこのバージョンの場合は arXiv:2607.08550v1 [cs.PL]) https://doi.org/10.48550/arXiv.2607.08550 詳細はこちら arXiv発行のDOIはDataCite経由です 提出履歴 From: Pierre Dantas [メール表示] [v1] 2026年7月9日 木曜日 14:42:15 UTC (44 KB) 全文リンク: ペーパーにアクセス: タイトル「ESBMC-Arduino: オープンハードウェアPLCの形式検証におけるデプロイメントギャップを埋める」のPDFを表示、Pierre Dantasと他の2名の著者によるPDF HTML（実験的） TeXソース ライセンス表示 現在のブラウジングコンテキスト: cs.PL < 前 | 次 > 新規 | 最近 | 2026-07 のブラウジングに変更: cs cs.AR cs.SY eess eess.SY 参考文献と引用 NASA ADS Google Scholar Semantic Scholar エクスポート BibTeX引用 読み込み中... BibTeX形式の引用 × 読み込み中... Data provided by: ブックマーク 参考文献ツール 参考文献と引用ツール 参考文献エクスプローラー 参考文献エクスプローラーを切り替える (エクスプローラーとは？) Connected Papers Connected Papersを切り替える (Connected Papersとは？) Litmaps Litmapsを切り替える (Litmapsとは？) scite.ai sciteスマート引用を切り替える (Smart Citationsとは？) コード、データ、メディア この記事に関連するコード、データ、メディア alphaXiv alphaXivを切り替える (alphaXivとは？) コードへのリンク コードファインダーを切り替える (CatalyzeXとは？) DagsHub DagsHubを切り替える (DagsHubとは？) GotitPub GotitPubを切り替える (GotitPubとは？) Huggingface Hugging Faceを切り替える (Huggingfaceとは？) ScienceCast ScienceCastを切り替える (ScienceCastとは？) デモ Replicate Replicateを切り替える (Replicateとは？) Spaces Hugging Face Spacesを切り替える (Spacesとは？) Spaces TXYZ.AIを切り替える (TXYZ.AIとは？) 関連論文 レコメンダーおよび検索ツール 影響力のある花へのリンク 影響力のある花 (影響力のある花とは？) コアレコメンダーを切り替える COREレコメンダー (COREとは？) 作者 会場 機関 トピック arXivラボについて arXivラボ: コミュニティ協力者との実験的なプロジェクト arXivラボは、協力者が当社のウェブサイトで直接新しいarXiv機能を開発および共有できるフレームワークです。arXivラボと協力する個人および組織は、オープンさ、コミュニティ、卓越性、ユーザーデータプライバシーという価値観を受け入れ、遵守しています。arXivはこれらの価値観にコミットしており、それらを遵守するパートナーのみと協力します。arXivコミュニティに価値をもたらすプロジェクトのアイデアがありますか？arXivラボの詳細をご覧ください。この論文の著者のうち、推薦者は誰ですか？ | MathJaxを無効にする (MathJaxとは？)