論文の概要: 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つの機能欠陥を明らかにする。
関連論文リスト
- 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) - Standardizing Structural Causal Models [80.21199731817698]
ベンチマークアルゴリズムのための内部標準構造因果モデル(iSCM)を提案する。
構成上、iSCMは$operatornameVar$-sortableではなく、実験的に示すように、$operatornameR2$-sortableではない。
論文 参考訳（メタデータ） (2024-06-17T14:52:21Z) - Towards Using Behavior Trees in Industrial Automation Controllers [41.94295877935867]
業界 4.0 パラダイムは、大量カスタマイズとサイバー物理生産システムへの移行を示している。
PLCソフトウェアには柔軟性がなく、低レベルのプログラムと高レベルのタスク指向制御フレームワークが統合されている。
本稿では, PLCプログラムに振舞い木を統合することにより, 産業制御ソフトウェア設計を改善する手法を提案する。
論文 参考訳（メタデータ） (2024-04-22T09:47:36Z) - Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。
仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。
実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
論文 参考訳（メタデータ） (2024-03-31T18:15:49Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳（メタデータ） (2023-09-25T15:42:18Z) - Transpiling RTL Pseudo-code of the POWER Instruction Set Architecture to
C for Real-time Performance Analysis on Cavatools Simulator [0.0]
本稿では,POWER命令セットアーキテクチャ(ISA)のRTL擬似コードをCコードに変換するためのトランスパイラフレームワークを提案する。
トランスパイラは、要件に準拠したCコードを生成することで、Cavatoolsシミュレータとの互換性を保証する。
提案するフレームワークは,RTL擬似コードをCavatoolsエコシステムにシームレスに統合し,総合的なパフォーマンス解析とPower ISAベースのコードの最適化を可能にする。
論文 参考訳（メタデータ） (2023-06-14T18:53:14Z) - ProgSG: Cross-Modality Representation Learning for Programs in
Electronic Design Automation [38.023395256208055]
高レベル合成(HLS)により、開発者はCとC++のソフトウェアコード形式で高レベルな記述をコンパイルできる。
HLSツールは相変わらず、プラグマで表されるマイクロアーキテクチャの決定を必要とする。
本稿では,ソースコードシーケンスのモダリティとグラフのモダリティを深く,きめ細かな方法で相互に相互作用させることができるProgSGを提案する。
論文 参考訳（メタデータ） (2023-05-18T09:44:18Z) - Structured Chain-of-Thought Prompting for Code Generation [48.43888515848583]
CoTプロンプト(Chain-of-Thought)は最先端のプロンプト技術である。
本研究では、構造化CoT(Structured CoTs)を提案し、コード生成のための新しいプロンプト技術であるSCoTプロンプトを提案する。
論文 参考訳（メタデータ） (2023-05-11T06:43:37Z) - Natural Language to Code Translation with Execution [82.52142893010563]
実行結果-プログラム選択のための最小ベイズリスク復号化。
そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
論文 参考訳（メタデータ） (2022-04-25T06:06:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。