論文の概要: K-ST: A Formal Executable Semantics of the Structured Text Language for
PLCs
- arxiv url: http://arxiv.org/abs/2202.04076v2
- Date: Tue, 12 Sep 2023 02:05:17 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-24 15:38:14.719609
- Title: K-ST: A Formal Executable Semantics of the Structured Text Language for
PLCs
- Title（参考訳）: K-ST:PLCのための構造化テキスト言語の形式的実行可能な意味論
- Authors: Kun Wang, Jingyi Wang, Christopher M. Poskitt, Xiangxiang Chen, Jun
Sun, and Peng Cheng
- Abstract要約: Kフレームワークで構造化テキスト(ST)の形式的実行可能なセマンティクスであるK-STを開発する。
K-STは高レベルの参照セマンティクスであり、異なるST実装の正確性と一貫性を評価するのに使用できる。
我々は、Githubから抽出した509のSTプログラムを実行し、既存の商用コンパイラと比較することで、K-STを検証する。
- 参考スコア（独自算出の注目度）: 10.993724354322657
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Programmable Logic Controllers (PLCs) are responsible for automating process
control in many industrial systems (e.g. in manufacturing and public
infrastructure), and thus it is critical to ensure that they operate correctly
and safely. The majority of PLCs are programmed in languages such as Structured
Text (ST). However, a lack of formal semantics makes it difficult to ascertain
the correctness of their translators and compilers, which vary from
vendor-to-vendor. In this work, we develop K-ST, a formal executable semantics
for ST in the K framework. Defined with respect to the IEC 61131-3 standard and
PLC vendor manuals, K-ST is a high-level reference semantics that can be used
to evaluate the correctness and consistency of different ST implementations. We
validate K-ST by executing 509 ST programs extracted from Github and comparing
the results against existing commercial compilers (i.e., CODESYS,
CX-Programmer, and GX Works2). We then apply K-ST to validate the
implementation of the open source OpenPLC platform, comparing the executions of
several test programs to uncover five bugs and nine functional defects in the
compiler.
- Abstract（参考訳）: PLC(Programmable Logic Controllers)は、多くの産業システム(製造業や公共インフラなど)におけるプロセス制御の自動化に責任を持つ。
PLCの大部分はStructured Text (ST) などの言語でプログラムされている。
しかし、形式的な意味論の欠如は、ベンダーからベンダーまで異なる翻訳者やコンパイラーの正確性を確認するのを難しくしている。
本研究では,K フレームワークにおける ST の形式的実行的意味論である K-ST を開発する。
IEC 61131-3標準とPLCベンダーマニュアルに関して定義されたK-STは、異なるST実装の正確性と一貫性を評価するために使用できる高レベルの参照セマンティクスである。
我々は、Githubから抽出した509のSTプログラムを実行し、既存の商用コンパイラ(CODESYS、CX-Programmer、GX Works2)と比較することで、K-STを検証する。
次に、オープンソースのOpenPLCプラットフォームの実装を検証するためにK-STを適用し、いくつかのテストプログラムの実行を比較して、コンパイラの5つのバグと9つの機能欠陥を明らかにする。
関連論文リスト
- EquiBench: Benchmarking Code Reasoning Capabilities of Large Language Models via Equivalence Checking [54.354203142828084]
本稿では,大規模言語モデルのコード推論能力を評価する新しい手法として等価チェックの課題を提案する。
EquiBenchは、4つのプログラミング言語と6つの等価カテゴリにまたがる2400のプログラムペアのデータセットである。
その結果,OpenAI o3-miniの精度は78.0%と高いことがわかった。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - A Multi-Agent Framework for Extensible Structured Text Generation in PLCs [9.555744065377148]
IEC 61131-3規格に準拠した高水準言語はPLCにとって重要なものである。
STの完全な意味論に関する包括的で標準化されたドキュメントが欠如していることは、言語の実装方法に矛盾をもたらしている。
ベンダー固有のSTコードの自動生成を目的としたLCMベースのアプローチであるAutoPLCを提案する。
論文 参考訳（メタデータ） (2024-12-03T12:05:56Z) - SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
CTCモデルであるSVTRv2を提案する。
SVTRv2は、テキストの不規則性に対処し、言語コンテキストを利用するための新しいアップグレードを導入した。
我々は,SVTRv2を標準ベンチマークと最近のベンチマークの両方で評価した。
論文 参考訳（メタデータ） (2024-11-24T14:21:35Z) - Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
本稿では,VeriFast で検証可能な C プログラムの仕様作成における OpenAI の GPT-4o モデルの有効性について検討する。
以上の結果から,GPT-4oで生成された仕様は機能的挙動を保っているが,検証に苦慮していることが明らかとなった。
論文 参考訳（メタデータ） (2024-11-04T17:44:11Z) - Training LLMs for Generating IEC 61131-3 Structured Text with Online Feedback [0.0]
本稿では,IEC 61131-3 構造化テキスト (ST) コード生成のための微調整 LLM へのアプローチを提案する。
このフレームワークは産業自動化アプリケーションに非常に適しており、最先端のモデルより優れている。
論文 参考訳（メタデータ） (2024-10-29T15:54:09Z) - 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) - NoviCode: Generating Programs from Natural Language Utterances by Novices [59.71218039095155]
初心者非プログラマによるAPIと自然言語記述を入力とする新しいNLプログラミングタスクであるNoviCodeを提示する。
我々は、NoviCodeがコード合成領域における挑戦的なタスクであることを示し、非技術的命令から複雑なコードを生成することは、現在のText-to-Codeパラダイムを超えている。
論文 参考訳（メタデータ） (2024-07-15T11:26:03Z) - C-LLM: Learn to Check Chinese Spelling Errors Character by Character [61.53865964535705]
本稿では,C-LLMを提案する。C-LLMは,文字による誤り文字のチェックを学習する中国語のスペルチェック手法である。
C-LLMは既存の方法よりも平均10%改善する。
論文 参考訳（メタデータ） (2024-06-24T11:16:31Z) - Towards Using Behavior Trees in Industrial Automation Controllers [41.94295877935867]
業界 4.0 パラダイムは、大量カスタマイズとサイバー物理生産システムへの移行を示している。
PLCソフトウェアには柔軟性がなく、低レベルのプログラムと高レベルのタスク指向制御フレームワークが統合されている。
本稿では, PLCプログラムに振舞い木を統合することにより, 産業制御ソフトウェア設計を改善する手法を提案する。
論文 参考訳（メタデータ） (2024-04-22T09:47:36Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳（メタデータ） (2023-09-25T15:42:18Z) - Structured Chain-of-Thought Prompting for Code Generation [48.43888515848583]
CoTプロンプト(Chain-of-Thought)は最先端のプロンプト技術である。
本研究では、構造化CoT(Structured CoTs)を提案し、コード生成のための新しいプロンプト技術であるSCoTプロンプトを提案する。
論文 参考訳（メタデータ） (2023-05-11T06:43:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。