論文の概要: 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ラダーダイアグラムの形式的検証
• Authors: Pierre Dantas, Lucas Cordeiro, Waldir Junior,
• 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)

関連論文リスト

• 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)
• 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)
• 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)

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

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