論文の概要: 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つの機能欠陥を明らかにする。
関連論文リスト
- 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) - When LLM-based Code Generation Meets the Software Development Process [50.82665351100067]
本稿では,ソフトウェア工学の確立した実践に触発されたコード生成フレームワークであるLCGを紹介する。
LLMエージェントは、LCGWaterfall、LCGTDD、LCGScrumといった様々なソフトウェアプロセスモデルをエミュレートする。
我々は,HumanEval,HumanEval-ET,MBPP,MBPP-ETの4つのコード生成ベンチマークでLCGを評価した。
論文 参考訳(メタデータ) (2024-03-23T14:04:48Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳(メタデータ) (2023-09-25T15:42:18Z) - A General Verification Framework for Dynamical and Control Models via
Certificate Synthesis [60.03938402120854]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳(メタデータ) (2023-09-12T09:37:26Z) - 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) - Code4Struct: Code Generation for Few-Shot Event Structure Prediction [55.14363536066588]
我々は,構造化予測タスクに対処するために,テキストから構造への変換機能を活用するCode4Structを提案する。
我々は、テキストをコードを使ってクラスオブジェクトとして表現できるイベント引数構造に変換するものとして、イベント引数抽出(EAE)を定式化する。
Code4Structは4,202インスタンスでトレーニングされた教師付きモデルに匹敵し、20ショットデータで29.5%の絶対F1でトレーニングされた現在のSOTA(State-of-the-art)を上回っている。
論文 参考訳(メタデータ) (2022-10-23T18:18:51Z) - Natural Language to Code Translation with Execution [82.52142893010563]
実行結果-プログラム選択のための最小ベイズリスク復号化。
そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
論文 参考訳(メタデータ) (2022-04-25T06:06:08Z) - Compilable Neural Code Generation with Compiler Feedback [43.97362484564799]
本稿では、言語モデルの微調整、コンパイル可能性強化、コンパイル可能性判定を含む、コンパイル可能なコード生成のための3段階パイプラインを提案する。
2つのコード生成タスクの実験は,提案手法の有効性を示し,平均44.18から89.18に,テキスト・コード生成では70.3から96.2に向上した。
論文 参考訳(メタデータ) (2022-03-10T03:15:17Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。