論文の概要: ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
- arxiv url: http://arxiv.org/abs/2606.18941v2
- Date: Thu, 18 Jun 2026 11:25:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-19 13:55:51.815361
- Title: ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
- Title（参考訳）: ESBMC-GraphPLC:SMTモデルチェックを用いたグラフPLCopen XMLラダーダイアグラムの形式的検証
- Abstract要約: PLCopen XML は IEC 61131-3 Ladder Diagram プログラムの2つのエンコード形式を定義している。
ESBMC-PLCはテキストフォーマットをサポートしていたが、グラフィカルなエクスポートを空のGOTO中間表現に解析した。
本稿では、このギャップをDFSベースのグラフィカルLDリゾルバで埋めるESBMC-GraphPLCを提案する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs: a textual encoding using <rung> elements, and a graphical encoding that represents rung logic as a directed graph of localId/refLocalId connections. ESBMC-PLC supported the textual format but parsed graphical exports from CONTROLLINO, Beremiz, and OpenPLC Editor into an empty GOTO intermediate representation, causing vacuous verification success. This paper presents ESBMC-GraphPLC, which closes this gap with a DFS-based graphical LD resolver. The resolver traverses the connection graph from leftPowerRail to each coil, extracts rung paths as Boolean contact conjunctions, and applies a three-tier I/O inference scheme. Ordering coils by rightPowerRail connectionPointIn sequence ensures SET coils process before RESET coils, matching IEC scan-cycle semantics. The graphical-to-IR conversion leaves the ESBMC backend unchanged. Validation on 3 graphical LD programs from CONTROLLINO/OpenPLC Editor shows all produce full GOTO IR with nondeterministic inputs and rung logic, versus the empty IR previously. All 3 verify SAFE at k=2 under 70ms. The 11 textual LD benchmarks are fully preserved, with no regression. Two Beremiz examples with no LD content or unsupported timer semantics are reported as discovered limitations. Artifact at Zenodo (DantasCordeiro2026graphical, doi:10.5281/zenodo.20699856).
- Abstract（参考訳）: PLCopen XMLは、IEC 61131-3ラダーダイアグラムプログラムの2つのエンコーディングフォーマットを定義している。
ESBMC-PLCはテキストフォーマットをサポートしていたが、CructoLino、Beremiz、OpenPLC Editorからのグラフィカルなエクスポートを空のGOTO中間表現に解析し、曖昧な検証に成功した。
本稿では、このギャップをDFSベースのグラフィカルLDリゾルバで埋めるESBMC-GraphPLCを提案する。
レゾルバは左PowerRailから各コイルへの接続グラフをトラバースし、ブール接触接続としてラングパスを抽出し、3層I/O推論スキームを適用する。
rightPowerRail connectionPointIn配列によるコイルの順序付け RESETコイルの前にSETコイルを確実に処理し、IECスキャンサイクルのセマンティクスと一致する。
グラフィカルからIRへの変換はESBMCのバックエンドをそのままにする。
ControlLINO/OpenPLC Editorによる3つのグラフィカルLDプログラムの検証では、すべてのGOTO IRが非決定論的入力とラング論理を持つ。
3つとも、SAFEをk=2で70ms以下で検証する。
11のテキストLDベンチマークは完全に保存されており、レグレッションはない。
LDを含まない2つのBeremiz例や、サポートされていないタイマーセマンティクスが発見された制限として報告されている。
禅道の工芸品(DantasCordeiro 2026graphical, doi:10.5281/zenodo.20699856)
関連論文リスト
- 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) - Generative Diffusion Models of Stochastic Graph Signals [74.4097723209053]
本稿では,条件付きグラフ信号生成モデルの問題に取り組み,単一の拡散フレームワークを用いてそれらに取り組む。
グラフトポロジとノード機能側情報に基づいて直接条件付きグラフ信号を描画するグラフニューラルネットワーク(GNN)によりパラメータ化された逆拡散過程を学習する。
本稿では,株価予測と最適無線リソース割り当てという2つの生成課題について,両領域で広範囲に数値計算を行った。
論文 参考訳（メタデータ） (2026-07-07T22:02:13Z) - ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor [0.0]
ESBMC-PLC+は、単一のESBMCバックエンドを介して3つの主要なIEC 61131-3入力フォーマットをサポートする最初のオープンソース検証フレームワークである。
ESBMC-PLC+ は PLCverif の入力カバレッジと一致し、より強力な保証を提供する。
論文 参考訳（メタデータ） (2026-06-22T19:13:02Z) - 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) - Reasoning to Align: Implicit Reasoning in Diffusion Transformers for Video Editing [55.211537893248675]
本稿では,2つの補完コンポーネントを中心に構築された暗黙の推論ビデオ編集用DiTフレームワークであるRVEDiTを提案する。
RVEDiTは最先端のベースラインを一貫して上回り、特にローカライズされた編集や構成的な編集において大きな利益を得ている。
論文 参考訳（メタデータ） (2026-05-23T17:22:14Z) - Mapping Text to Multiplex Graph: Prompt Compression as Lévy Walk-Guided Graph Pruning [55.43705665875779]
RAGPは、多重グラフ上の冗長性を考慮したグラフプルーニングとして、即時圧縮を定式化する。
LongBenchの実験では、RAGPは平均スコア49.3を4倍の圧縮比で達成している。
論文 参考訳（メタデータ） (2026-05-04T01:41:31Z) - Semi-supervised Instruction Tuning for Large Language Models on Text-Attributed Graphs [62.544129365882014]
本稿では,SIT-Graph というグラフ学習用セミ教師付きインストラクションチューニングパイプラインを提案する。
SIT-Graphはモデルに依存しず、LSMを予測子として利用するグラフ命令チューニングメソッドにシームレスに統合することができる。
SIT-Graphは、最先端グラフチューニング手法に組み込むと、テキスト分散グラフベンチマークの性能を大幅に向上することを示した。
論文 参考訳（メタデータ） (2026-01-19T08:10:53Z) - Zero-shot Graph Reasoning via Retrieval Augmented Framework with LLMs [15.558119182035995]
検索型拡張フレームワーク(GRRAF)を用いた新しい学習不要なグラフ推論手法を提案する。
GRRAFは、大規模な言語モデル(LLM)のコード生成機能とともに、検索拡張生成(RAG)を活用して、幅広いグラフ推論タスクに対処する。
GraphInstructデータセットの実験的評価により、ほとんどのグラフ推論タスクにおいて、GRRAFが100%の精度を達成することが明らかになった。
論文 参考訳（メタデータ） (2025-09-16T06:58:58Z) - See it. Say it. Sorted: Agentic System for Compositional Diagram Generation [0.5079602839359522]
スケッチ・トゥ・ダイアグラムの生成について研究し、粗い手書きスケッチを正確な構成図に変換する。
視覚言語モデル(VLM)とLarge Language Models(LLM)を結合した学習自由エージェントシステムSorted.を紹介する。
このシステムは、批判的VLMが小さな定性的な編集セットを提案する反復ループを実行し、複数の候補LPMが様々な戦略で更新を合成する。
この設計は、不安定な数値推定よりも定性的推論を優先し、大域的制約(例えば、アライメント、接続性)を保存し、自然に人間のループをサポートする。
論文 参考訳（メタデータ） (2025-08-21T04:20:36Z) - Align-GRAG: Reasoning-Guided Dual Alignment for Graph Retrieval-Augmented Generation [79.75818239774952]
大きな言語モデル(LLM)は目覚ましい能力を示しているが、幻覚や時代遅れの情報といった問題に苦戦している。
Retrieval-augmented Generation (RAG) は、情報検索システム(IR)を用いて、外部知識のLLM出力を基底にすることで、これらの問題に対処する。
本稿では、検索後句における新しい推論誘導二重アライメントフレームワークであるAlign-GRAGを提案する。
論文 参考訳（メタデータ） (2025-05-22T05:15:27Z) - An Efficient Post-hoc Framework for Reducing Task Discrepancy of Text Encoders for Composed Image Retrieval [34.065449743428005]
Composed Image Retrieval (CIR) は、参照画像と条件付きテキストに基づいてターゲット画像を取得することを目的としており、制御可能な画像検索を可能にする。
従来のZero-Shot (ZS) CIRメソッドは、画像埋め込みをテキストトークン埋め込み空間に投影することで、高価なトレーニング用CIRトリプルの必要性を回避している。
本稿では,プロジェクションベースのCIR手法を補完する効率的なテキストのみのフレームワークであるReduceing Taskrepancy of Texts (RTD)を紹介する。
論文 参考訳（メタデータ） (2024-06-13T14:49:28Z) - Visual Delta Generator with Large Multi-modal Models for Semi-supervised Composed Image Retrieval [50.72924579220149]
Composed Image Retrieval (CIR)は、提供されるテキスト修正に基づいて、クエリに似たイメージを取得するタスクである。
現在の技術は、基準画像、テキスト、ターゲット画像のラベル付き三重項を用いたCIRモデルの教師あり学習に依存している。
本稿では,参照とその関連対象画像を補助データとして検索する半教師付きCIR手法を提案する。
論文 参考訳（メタデータ） (2024-04-23T21:00:22Z) - DiagrammerGPT: Generating Open-Domain, Open-Platform Diagrams via LLM Planning [62.51232333352754]
テキスト・ツー・イメージ(T2I)世代はここ数年で著しい成長を遂げている。
それにもかかわらず、T2Iモデルでダイアグラムを生成する作業はほとんど行われていない。
本稿では,新しい2段階のテキスト・ツー・ダイアグラム生成フレームワークであるDiagrammerGPTを紹介する。
我々のフレームワークは、既存のT2Iモデルを上回る精度で、より正確なダイアグラムを生成する。
論文 参考訳（メタデータ） (2023-10-18T17:37:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。