論文の概要: ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking

• arxiv url: http://arxiv.org/abs/2606.15461v1
• Date: Sat, 13 Jun 2026 20:39:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-16 16:21:33.588293
• Title: ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking
• Title（参考訳）: ESBMC-PLC:SMTモデル検査を用いたIEC 61131-3ラダーダイアグラムプログラムの形式的検証
• Authors: Pierre Dantas, Lucas Cordeiro, Waldir Junior,
• Abstract要約: 本稿では、ネイティブLDサポート(PLCopen XMLフォーマット)を備えた最初のオープンソース形式検証器であるESBMC-PLCについて述べる。 ESBMC-PLCはLDラングをGOTO IRに変換し、PLCスキャンサイクルを非決定論的入力による時(真の)証明ループとしてモデル化し、境界モデルチェックやk-インダクションによる安全性チェックを行う。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: PLCs execute safety-critical programs across industrial sectors. The dominant PLC notation, ladder diagram (LD) per IEC 61131-3, remains absent from formal verification: SMT-based model checkers cannot process LD's rung-and-coil graphics. This paper presents ESBMC-PLC, the first open-source formal verifier with native LD support (PLCopen XML format), implemented as a new ESBMC frontend. ESBMC-PLC translates LD rungs to GOTO IR, models the PLC scan cycle as a while(true) loop with nondeterministic inputs, and checks safety properties via SMT-based bounded model checking or k-induction. A five-property YAML language (mutual_exclusion, invariant, absence, response, reachability) avoids temporal logic. A survey of 22 studies (2020-2026) identifies four research gaps; ESBMC-PLC closes two of them. Evaluation on 13 benchmarks (6 domains, 3 sources - including deployed CONTROLLINO PLCs and MathWorks Simulink PLC Coder) shows correct classification across 61 properties: all 9 author-constructed programs (Categories A/B) as expected, all 4 vendor programs (Category C) correctly unlabeled, with 8 bugs found (actionable counterexamples), 7 unbounded k-induction proofs, all runs under 60ms on Apple Silicon. Feature comparison with PLCverif shows that ESBMC-PLC is the only open-source tool that combines native LD, k-induction, and SMT bit-vector semantics.
• Abstract（参考訳）: PLCは産業セクター全体で安全クリティカルなプログラムを実行する。 IEC 61131-3 あたりの PLC 表記のラダーダイアグラム (LD) は、正式な検証に欠ける: SMT ベースのモデルチェッカーは、LD のrung-and-coil グラフィックを処理できない。 本稿では,新しいESBMCフロントエンドとして実装されたLDサポート(PLCopen XMLフォーマット)を備えた初のオープンソース形式検証器であるESBMC-PLCについて述べる。 ESBMC-PLCはLDラングをGOTO IRに変換し、PLCスキャンサイクルを非決定論的入力を持つ while(true)ループとしてモデル化し、SMTベースの有界モデルチェックやk-inductionを通じて安全性チェックを行う。 5種類のYAML言語(mutual_exclusion, invariant, absence, response, reachability)は、時間論理を避ける。 22の研究(2020-2026)による調査では、4つの研究ギャップが特定され、ESBMC-PLCは2つを閉じている。 13のベンチマーク(ドメイン6つ、ソース3つ、デプロイされたコントロールLINO PLCとMathWorks Simulink PLC Coderを含む)の評価では、61のプロパティの正確な分類が示されている。 PLCverifと比較すると、ESBMC-PLCはネイティブLD、k-induction、SMTビットベクトルセマンティクスを組み合わせた唯一のオープンソースツールである。

関連論文リスト

• Off-the-Shelf LLMs as Process Scorers: Training-Free Alternative to PRMs for Mathematical Reasoning [51.88950852117154]
  Chunk-Level Guided Generationは、既製の大規模言語モデルをプロセススコアラとして使用する、トレーニング不要の代替手段である。 本研究では,系統的な長さバイアスのため,大モデル確率の可変長推論ステップが信頼できないことを示す。 Chunk-Level Guided Generation は PRM guided search よりもかなり短い推論トレースを生成する。
  論文  参考訳（メタデータ） (2026-06-01T04:43:36Z)
• One Step Further: Understanding PLC Binaries Through Cross-Platform Reverse Engineering and Function-Level Semantic Analysis [7.990445011559295]
  PLC-BinXはクロスプラットフォームのPLCバイナリ理解のためのBCAワークフローである。 10倍のプログラムレベルでの評価では、PLC-BinXはツールチェーン予測において100.00%の精度、リコール、F1を達成する。 その結果、PLC-BinXはクロスプラットフォームのPLCバイナリ理解に効果的かつ解釈可能なアプローチを提供することが示された。
  論文  参考訳（メタデータ） (2026-05-17T11:19:47Z)
• TSCG: Deterministic Tool-Schema Compilation for Agentic LLM Deployments [0.0]
  生産エージェントフレームワークは、言語モデルによる解釈ではなく、機械解析用に設計されたフォーマットであるMPPとしてツールスキーマを送信する。 小型モデル(4B-14B)では、このプロトコルのミスマッチが、本番サイズでのツール使用障害の大部分の原因となっている。 本稿では,このミスマッチをAPI境界で解決する決定論的ツールスキーマコンパイラTSCGを提案する。
  論文  参考訳（メタデータ） (2026-05-04T15:35:45Z)
• LFM2 Technical Report [87.58431408281973]
  LFM2は、デバイス上での効率的なデプロイと強力なタスク機能を実現するために設計された、Liquid Foundation Modelsのファミリーである。 LFM2ファミリーは350M-8.3Bパラメータをカバーしており、密度の高いモデル(350M, 700M, 1.2B, 2.6B)と試験用混合物(合計8.3B, 1.5B)を含んでいる。 視覚遅延タスクのためのLFM2-VL,音声のためのLFM2-Audio,検索のためのLFM2-ColBERTを構築した。
  論文  参考訳（メタデータ） (2025-11-28T17:56:35Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  生成のための教師なし共形推論フレームワークを提案する。 我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。 その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
  論文  参考訳（メタデータ） (2025-09-26T23:40:47Z)
• Bridging the PLC Binary Analysis Gap: A Cross-Compiler Dataset and Neural Framework for Industrial Control Systems [14.826593801448032]
  PLC-BEADは4つの主要な産業用コンパイラにまたがる700以上のPLCプログラムから2431のコンパイル済みバイナリを含むデータセットである。 この新しいデータセットは、それぞれのバイナリを独自のStructured Textソースコードと標準化された機能ラベルと一意にペアリングする。 バイナリコード解析のためのトランスフォーマーベースのフレームワークであるPLCEmbedを用いて,データセットの有用性を実証する。
  論文  参考訳（メタデータ） (2025-02-27T03:27:37Z)
• 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)
• K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs [10.993724354322657]
  Kフレームワークで構造化テキスト(ST)の形式的実行可能なセマンティクスであるK-STを開発する。 K-STは高レベルの参照セマンティクスであり、異なるST実装の正確性と一貫性を評価するのに使用できる。 我々は、Githubから抽出した509のSTプログラムを実行し、既存の商用コンパイラと比較することで、K-STを検証する。
  論文  参考訳（メタデータ） (2022-02-08T17:34:08Z)

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

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