論文の概要: ESBMC-PLC+: A Unified IEC~61131-3 Formal Verification Framework as a PLCverif Successor

• arxiv url: http://arxiv.org/abs/2606.23870v1
• Date: Mon, 22 Jun 2026 19:13:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-24 22:16:48.64014
• Title: ESBMC-PLC+: A Unified IEC~61131-3 Formal Verification Framework as a PLCverif Successor
• Title（参考訳）: ESBMC-PLC+: PLCverif 継承器としての IEC~61131-3 形式検証フレームワーク
• Authors: Pierre Dantas, Lucas Cordeiro, Waldir Junior,
• Abstract要約: ESBMC-PLC+は、単一のESBMCバックエンドを介して3つの主要なIEC 61131-3入力フォーマットをサポートする最初のオープンソース検証フレームワークである。 ESBMC-PLC+ は PLCverif の入力カバレッジと一致し、より強力な保証を提供する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: PLCverif is the most mature open-source platform for PLC formal verification, developed at CERN and in production use since 2019. Yet it has two fundamental limitations: no support for Ladder Diagram (LD) programs, the dominant PLC notation, and reliance on CBMC as its primary backend, which restricts verification to bounded proofs. The PLCverif authors themselves identified ESBMC as the appropriate backend improvement. Prior work established ESBMC-PLC (a textual LD frontend with k-induction) and ESBMC-GraphPLC (graphical PLCopen XML support); together, they cover LD with unbounded proofs but not Structured Text (ST), and graphical LD with timer/counter function blocks remains unverifiable. This paper presents ESBMC-PLC+, a unified framework that closes both gaps: (1) an ST/SCL frontend via the MATIEC IEC 61131-3 compiler, routing C-compiled ST to ESBMC with nondeterministic input modeling and YAML property injection; (2) function block state semantics for graphical LD, extending the DFS resolver to model TON/TOF/TP timers, CTU/CTD counters, and R_TRIG/F_TRIG edge triggers as persistent scan-cycle state variables in the GOTO IR. ESBMC-PLC+ is the first open-source PLC verification framework to support all three major IEC 61131-3 input formats via a single ESBMC backend, enabling k-induction-unbounded safety proofs. A feature comparison with PLCverif and experimental evaluation on 8 benchmark programs, including programs with up to 8 integer timers, shows that ESBMC-PLC+ matches PLCverif's input coverage while providing stronger guarantees. Against nuXmv's BDD backend, ESBMC-PLC+ is 400-2,000x faster on timer programs and completes proofs where nuXmv BDD times out at 120s.
• Abstract（参考訳）: PLCverifは、CERNで開発され、2019年から実運用で使用されている、PLC形式検証のための最も成熟したオープンソースプラットフォームである。 しかし、Ladder Diagram (LD) プログラムのサポートなし、支配的な PLC 表記、CBMC を主要なバックエンドとして依存し、検証を有界証明に制限する、という2つの基本的な制限がある。 PLCverifの著者自身はESBMCを適切なバックエンドの改善とみなしている。 以前は ESBMC-PLC (k-induction 付きテキストLDフロントエンド) と ESBMC-GraphPLC (グラフィック PLCopen XML サポート) を確立していた。 本稿では,(1)MATIEC IEC 61131-3コンパイラによるST/SCLフロントエンド,(2)非決定論的入力モデリングとYAMLプロパティインジェクションによるC-コンパイルST to ESBMC,(2)グラフィカルLDのための関数ブロック状態セマンティクス,DFSリゾルバをTON/TOF/TPタイマ,CTU/CTDカウンタ,R_TRIG/F_TRIGエッジトリガの2つのギャップを埋める統合フレームワークであるESBMC-PLC+を提案する。 ESBMC-PLC+は、単一のESBMCバックエンドを介して3つの主要なIEC 61131-3入力フォーマットすべてをサポートする最初のオープンソースのPLC検証フレームワークである。 最大8つの整数タイマーを持つプログラムを含む8つのベンチマークプログラムにおいて、PLCverifと機能比較を行い、ESBMC-PLC+がPLCverifの入力カバレッジと一致し、より強力な保証を提供することを示した。 nuXmvのBDDバックエンドに対して、ESBMC-PLC+はタイマープログラムでは400-2000倍高速で、nuXmv BDDが120秒で倍増する証明を完成させている。

関連論文リスト

• ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking [0.0]
  PLCopen XML は IEC 61131-3 Ladder Diagram プログラムの2つのエンコード形式を定義している。 ESBMC-PLCはテキストフォーマットをサポートしていたが、グラフィカルなエクスポートを空のGOTO中間表現に解析した。 本稿では、このギャップをDFSベースのグラフィカルLDリゾルバで埋めるESBMC-GraphPLCを提案する。
  論文  参考訳（メタデータ） (2026-06-17T11:22:34Z)
• 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)
• GLM-OCR Technical Report [65.42028025507491]
  GLM-OCRは実世界の文書理解のために設計された効率的なコンパクトモデルである。 CogViTビジュアルエンコーダとGLM言語デコーダを組み合わせることで、計算効率と認識性能のバランスが強い。 公開ベンチマークと産業シナリオの大規模な評価は、GLM-OCRが競争力や最先端のパフォーマンスを達成することを示している。
  論文  参考訳（メタデータ） (2026-03-11T15:55:47Z)
• Preserving Cross-Modal Consistency for CLIP-based Class-Incremental Learning [77.82901519692378]
  クラスインクリメンタルラーニング(CIL)は、モデルが獲得した知識を忘れることなく、シーケンシャルなタスクから新しいカテゴリを継続的に学習することを可能にする。 視覚エンコーダの適応とテキストソフトプロンプトの最適化を分離するCLIPベースのCILのための2段階フレームワークであるDMCを提案する。 CIFAR-100, Imagenet-R, CUB-200, UCF-101 の大規模な実験により, DMC と DMC-OT の両者が最先端の性能を発揮することが示された。
  論文  参考訳（メタデータ） (2025-11-14T05:36:36Z)
• Towards Effective and Efficient Non-autoregressive Decoding Using Block-based Attention Mask [74.64216073678617]
  AMDはアテンションマスクを用いて隠された出力ラベルの連続ブロック内で並列NAR推論を行う。 ビームサーチアルゴリズムは、CTC、ARデコーダ、AMD確率の動的融合を利用するように設計されている。 LibriSpeech-100hrコーパスの実験では、AMDモジュールを組み込んだトリパルタイトデコーダが最大1.73倍のデコード速度比を生み出すことを示唆している。
  論文  参考訳（メタデータ） (2024-06-14T13:42:38Z)
• Towards Using Behavior Trees in Industrial Automation Controllers [41.94295877935867]
  業界 4.0 パラダイムは、大量カスタマイズとサイバー物理生産システムへの移行を示している。 PLCソフトウェアには柔軟性がなく、低レベルのプログラムと高レベルのタスク指向制御フレームワークが統合されている。 本稿では, PLCプログラムに振舞い木を統合することにより, 産業制御ソフトウェア設計を改善する手法を提案する。
  論文  参考訳（メタデータ） (2024-04-22T09:47:36Z)

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

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