論文の概要: 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 形式検証フレームワーク
- 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秒で倍増する証明を完成させている。
関連論文リスト
- PLC-Bin2Src: Retrieving Corresponding Structured Text Source Files for PLC Binaries [8.479104710721645]
PLC開発者は既存のコンポーネントやサードパーティのライブラリを再利用して、新しいアプリケーションの開発コストを削減している。
binary2source matchingは、候補のソースリポジトリからPLCバイナリに対応するStructured Text (ST)ソースファイルを取得することができる。
我々は,CODESYS,GEB,OpenPLC v2,OpenPLC v3で生成されたバイナリの対応するSTソースファイルを検索する,クロスプラットフォームのバイナリ2ソースマッチングフレームワークであるPLC-Bin2Srcを提案する。
論文 参考訳（メタデータ） (2026-09-08T10:52:46Z) - 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) - TempRet: Temporal Enhancement and Two-Stage Reranking for CVPR 2026 EPIC-KITCHENS-100 Multi-Instance Retrieval Challenge [71.10535279591527]
我々は,CVPR 2026 EPIC-KITCHENS-100 MIRチャレンジに対して,TempRetと呼ばれるソリューションを提示する。
当社のアプローチは,CLIPベースのデュアルエンコーダのバックボーン上に構築されており,時間的および横断的な課題に対処するための2つの重要なコンポーネントを導入している。
EK-100 MIRベンチマークでは,平均mAPは67.97%,平均nDCGは82.92%であった。
論文 参考訳（メタデータ） (2026-05-23T08:37:39Z) - 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) - GLM-OCR Technical Report [65.42028025507491]
GLM-OCRは実世界の文書理解のために設計された効率的なコンパクトモデルである。
CogViTビジュアルエンコーダとGLM言語デコーダを組み合わせることで、計算効率と認識性能のバランスが強い。
公開ベンチマークと産業シナリオの大規模な評価は、GLM-OCRが競争力や最先端のパフォーマンスを達成することを示している。
論文 参考訳（メタデータ） (2026-03-11T15:55:47Z) - FluxMem: Adaptive Hierarchical Memory for Streaming Video Understanding [49.23912975740968]
FluxMemは階層的な2段階の設計を通じて冗長な視覚記憶を適応的に圧縮する。
既存のオンラインビデオベンチマークで、最先端の結果を新たに達成する。
強力なオフライン性能を維持し、MLVUで73.1を達成し、65%のビジュアルトークンを使用する。
論文 参考訳（メタデータ） (2026-03-02T17:16:47Z) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。