論文の概要: A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs

• arxiv url: http://arxiv.org/abs/2609.18994v1
• Date: Fri, 17 Jul 2026 15:47:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-28 05:09:55.589283
• Title: A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs
• Title（参考訳）: IEC 61131-3ラダーダイアグラムプログラムの形式検証のためのベンチマークスイートとグラウンドトルース手法
• Abstract要約: 本稿では,Programmable Logic Controller (PLC)プログラムの形式検証のための最初のベンチマークスイートを提案する。 当社のスイートは,10の産業ドメインにわたる83の変種で50のプログラムで構成されています。 中心的な方法論的貢献は三部構成の地学の分野である。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present the first benchmark suite for formal verification of Programmable Logic Controller (PLC) programs that combines controlled ground truth with coverage of both textual (Structured Text, ST) and graphical (Ladder Diagram, LD) IEC 61131-3 encodings. Despite growing support for tools, the field lacks standard evaluation benchmarks: existing corpora omit formal properties or graphical dialects, and private program sets preclude reproducible measurement of progress. Our suite comprises 50 programs in 83 variants across ten industrial domains, provided in PLCopen Extensible Markup Language (XML) and ST, each paired with a formal property, machine-checkable expected verdict, and violation witness in the Software Verification Competition (SV-COMP) format. The central methodological contribution is a tripartite ground-truth discipline - verdicts are established by construction, fault injection, or audited cross-tool consensus - motivated by a concrete failure mode where the obvious safety property misclassifies all attacks from two public logic-bomb corpora as safe due to invisible non-termination. Reference verdicts are obtained with the Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v8.4 from source: all 25 graphical benchmarks execute, and 43 of 45 accepted variants match recorded verdicts. On the finite-state fragment (21 benchmarks), nuXmv - a model checker with unrelated decision procedures - agrees on all 24 interlock variants and resolves two benchmarks ESBMC-PLC leaves unknown, confirming tool-neutral ground truth and discriminative power. Porting exposes format and semantics fragmentation: front-ends accept different serializations, and timer semantics vary across tools - phenomena the suite is designed to reveal. The corpus, schema, validator, and recheck harness are released as open artifacts.
• Abstract（参考訳）: 本稿では,制御された基底真理とテキスト(構造化テキスト,ST)とグラフィカル(ラダーダイアグラム,LD)IEC 61131-3エンコーディングの両方をカバーするPLCプログラムの形式検証のための最初のベンチマークスイートを提案する。 既存のコーパスは形式的プロパティやグラフィカルな方言を省略し、プライベートプログラムセットは再現可能な進捗測定を妨げている。 PLCopen Extensible Markup Language (XML) と ST で提供される,10の産業ドメインにわたる50のプログラムからなり,それぞれに形式的プロパティ,マシンチェック可能な予測判断,ソフトウェア検証コンペティション (SV-COMP) フォーマットの違反証書が組み合わされている。 建設、フォールトインジェクション、監査済みのクロスツールコンセンサスによって判断が確立され、明らかな安全性が2つのパブリックロジックボムコーパスからの攻撃を、目に見えない非終端によって安全であると誤分類する、具体的な障害モードによって動機付けられている。 SMTベースのコンテキスト境界モデルチェッカー (ESBMC) v8.4 をソースとして、25のグラフィカルベンチマークが全て実行され、45の変種のうち43が記録された評定と一致している。 有限状態フラグメント(21ベンチマーク)では、無関係な決定手順を持つモデルチェッカーであるnuXmvが24のインターロック変種すべてに合意し、2つのベンチマークであるESBMC-PLCが未知のまま残っており、ツールニュートラル基底真理と識別力を確認している。 フロントエンドは異なるシリアライゼーションを受け入れ、タイマーのセマンティクスはツールによって異なります。 コーパス、スキーマ、バリデータ、リチェックハーネスはオープンアーティファクトとしてリリースされる。

関連論文リスト

• ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking [0.0]
  本稿では、ネイティブLDサポート(PLCopen XMLフォーマット)を備えた最初のオープンソース形式検証器であるESBMC-PLCについて述べる。 ESBMC-PLCはLDラングをGOTO IRに変換し、PLCスキャンサイクルを非決定論的入力による時(真の)証明ループとしてモデル化し、境界モデルチェックやk-インダクションによる安全性チェックを行う。
  論文  参考訳（メタデータ） (2026-06-13T20:39:49Z)
• ClawForge: Generating Executable Interactive Benchmarks for Command-Line Agents [59.626170560327274]
  textbfClawForgeは、ステートコンフリクト下で実行可能なコマンドラインカテゴリのためのジェネレータベースのベンチマークフレームワークである。 私たちはこのフレームワークをClawForge-Bench(17のシナリオ、6の能力カテゴリ)としてインスタンス化します。
  論文  参考訳（メタデータ） (2026-05-13T21:34:08Z)
• Symfrog-512: High-Capacity Sponge-Based AEAD Cipher (1024-bit State) [0.0]
  この提案には、決定論的テストベクタと再現可能なベンチマークスイートとともに、完全なリファレンス実装が含まれている。 AEADの構築は、ドメイン分離、レートとキャパシティの選択、タグ生成、参照CLIで使用される正確なファイルフォーマットなど、完全に規定されている。 報告されたパフォーマンス数値は、ドキュメンテーションされたハードウェアとコンパイラ設定の下で、組み込みのベンチマークツールによって生成される。
  論文  参考訳（メタデータ） (2026-02-19T23:39:54Z)
• CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
  隠れアクティベーションの軌跡内の幾何的に分離可能なシグネチャとして解の正しさが符号化されていることを示す。 ClUE は LLM-as-a-judge ベースラインを一貫して上回り、候補者の再選において近代的な信頼に基づく手法に適合または超えている。
  論文  参考訳（メタデータ） (2025-10-02T02:14:33Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。 このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。 19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。