論文の概要: Verifying Correctness of PLC Software during System Evolution using Model Containment Approach

• arxiv url: http://arxiv.org/abs/2509.05596v1
• Date: Sat, 06 Sep 2025 04:45:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-09 14:07:03.601786
• Title: Verifying Correctness of PLC Software during System Evolution using Model Containment Approach
• Title（参考訳）: モデル含みアプローチによるPLCソフトウェアのシステム進化過程における正当性検証
• Authors: Soumyadip Bandyopadhyay, Santonu Sarkar,
• Abstract要約: そこで本研究では,PLCソフトウェアのアップグレード版の正当性を保証するための検証に基づく手法を提案する。 我々は,自家製のペトリネット型封じ込めチェッカーを開発した。 当社のアプローチを,ソフトウェアアップグレードに一般的なツールであるVerifAPSと比較し,約4倍のパフォーマンス向上を確認した。
• 参考スコア（独自算出の注目度）: 22.261628532402067
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Upgradation of Programmable Logic Controller (PLC) software is quite common to accommodate evolving industrial requirements. Verifying the correctness of such upgrades remains a significant challenge. In this paper, we propose a verification-based approach to ensure the correctness of the existing functionality in the upgraded version of a PLC software. The method converts the older and the newer versions of the sequential function chart (SFC) into two Petri net models. We then verify whether one model is contained within another, based on a novel containment checking algorithm grounded in symbolic path equivalence. For this purpose, we have developed a home-grown Petri net-based containment checker. Experimental evaluation on 80 real-world benchmarks from the OSCAT library highlights the scalability and effectiveness of the framework. We have compared our approach with verifAPS, a popular tool used for software upgradation, and observed nearly 4x performance improvement.
• Abstract（参考訳）: Programmable Logic Controller (PLC) ソフトウェアのアップグレードは、進化する産業的要求に対応するために非常に一般的である。 このようなアップグレードの正しさを検証することは、依然として大きな課題である。 本稿では,PLCソフトウェアのアップグレード版における既存機能の正当性を保証するための検証に基づく手法を提案する。 この手法は、逐次関数チャート(SFC)の古いバージョンと新しいバージョンを2つのペトリネットモデルに変換する。 次に,シンボルパス同値性に基づく新しい包絡チェックアルゴリズムに基づいて,あるモデルが他のモデルに含まれているかどうかを検証する。 そこで我々は,自家製のペトリネット型封じ込めチェッカーを開発した。 OSCATライブラリの80の実世界のベンチマークに関する実験的評価は、フレームワークのスケーラビリティと有効性を強調している。 当社のアプローチを,ソフトウェアアップグレードに一般的なツールであるVerifAPSと比較し,約4倍のパフォーマンス向上を確認した。

関連論文リスト

• Machine Learning Pipeline for Software Engineering: A Systematic Literature Review [0.0]
  この系統的な文献レビューは、ソフトウェア工学(SE)用に設計された最先端の機械学習パイプラインを検証している。 この結果から,データバランシングのためのSMOTEなどの堅牢な前処理がモデルの信頼性を向上させることが示唆された。 ランダムフォレストやグラディエントブースティングのようなアンサンブルメソッドはタスク間でパフォーマンスを支配します。 Best Arithmetic Mean (BAM)のような新しいメトリクスはニッチなアプリケーションに現れている。
  論文  参考訳（メタデータ） (2025-07-31T15:37:30Z)
• VeriReason: Reinforcement Learning with Testbench Feedback for Reasoning-Enhanced Verilog Generation [9.07044866283158]
  本稿では,教師付き微調整とガイド・リワード近似最適化(GRPO)によるRTL生成のための強化学習を統合するフレームワークであるVeriReasonを紹介する。 VerilogEvalベンチマークでは、VeriReasonは83.1%の機能的正当性を提供しており、比較可能なサイズのモデルと、GPT-4 Turboのようなはるかに大きな商用システムの両方を上回っている。 VeriReasonは、Verilog生成のための強化学習と明示的な推論機能をうまく統合する最初のシステムであり、自動RTL合成のための新しい最先端技術を確立している。
  論文  参考訳（メタデータ） (2025-05-17T05:25:01Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)
• Agents4PLC: Automating Closed-loop PLC Code Generation and Verification in Industrial Control Systems using LLM-based Agents [27.097029139195943]
  Agents4PLCは、PLCコード生成とコードレベルの検証を自動化する新しいフレームワークである。 まず、検証可能なPLCコード生成領域のベンチマークを作成する。 そして、自然言語の要件から、人間によって記述された形式仕様と参照PLCコードへ移行する。
  論文  参考訳（メタデータ） (2024-10-18T06:51:13Z)
• CodeDPO: Aligning Code Models with Self Generated and Verified Source Code [52.70310361822519]
  我々は、コード生成に好み学習を統合するフレームワークであるCodeDPOを提案し、コードの正確性と効率性という2つの重要なコード優先要因を改善した。 CodeDPOは、コードとテストケースを同時に生成、評価するセルフジェネレーション・アンド・バリデーションメカニズムを利用して、新しいデータセット構築方法を採用している。
  論文  参考訳（メタデータ） (2024-10-08T01:36:15Z)
• Uncovering the Hidden Cost of Model Compression [43.62624133952414]
  視覚プロンプティングは、コンピュータビジョンにおける伝達学習の重要な方法として登場した。 モデル圧縮は視覚的プロンプトベース転送の性能に有害である。 しかし、量子化によってモデルが圧縮されるとき、キャリブレーションに対する負の効果は存在しない。
  論文  参考訳（メタデータ） (2023-08-29T01:47:49Z)
• Consensus-Adaptive RANSAC [104.87576373187426]
  本稿では,パラメータ空間の探索を学習する新しいRANSACフレームワークを提案する。 注意機構は、ポイント・ツー・モデル残差のバッチで動作し、軽量のワンステップ・トランスフォーマーで見いだされたコンセンサスを考慮するために、ポイント・ツー・モデル推定状態を更新する。
  論文  参考訳（メタデータ） (2023-07-26T08:25:46Z)
• Model-based adaptation for sample efficient transfer in reinforcement learning control of parameter-varying systems [1.8799681615947088]
  我々はモデルに基づく制御のアイデアを活用し、強化学習アルゴリズムのサンプル効率問題に対処する。 また,本手法は強化学習のみでの微調整よりもサンプリング効率が高いことを示した。
  論文  参考訳（メタデータ） (2023-05-20T10:11:09Z)

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

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