文献

J-GLOBAL ID：201902281782926449   整理番号：19A0519144

Simulink設計を用いたPLCプログラムのモデルベース検証【JST・京大機械翻訳】

Model-based verification of PLC programs using Simulink design

著者 (3件)： He Nannan (Department of Electrical and Computer Engineering Technology, Minnesota State University at Mankato, United States) ,  Oke Victor (Department of Electrical and Computer Engineering Technology, Minnesota State University at Mankato, United States) ,  Allen Gale (Department of Electrical and Computer Engineering Technology, Minnesota State University at Mankato, United States)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2016  号： EIT  ページ： 0211-0216  発行年： 2016年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： プログラマブル論理制御装置(PLC)は,安全に重要な産業プロセスに広く適用されている。PLCプログラムの自動検証は,制御システム技術者にとって挑戦的な課題である。PLCプログラムを検証するためのSimulink設計モデルの突然変異に基づく検証法を提案した。本研究では,構造化テキスト(ST)言語でコード化されたPLCプログラムを,MathworksからのツールSimulink PLC Coderを用いてSimulinkモデルから自動的に生成すると仮定した。システム設計モデルとしてSimulink図を利用した。Simulinkは複雑な事象駆動アプリケーションを開発するための強力な設計ツールである。設計モデルの機能特性を形式的に検証するために,Gen-Autoと呼ばれる検証モデルコンパイラを,SimulinkモデルをCコードに自動的に変換するために適用した。チェックされるべき特性は,翻訳されたCコードに挿入されるC主張としても翻訳される。次に,主張を装備した生成Cコードを,CBMCと呼ばれるCプログラムのための有界モデル検査ツールで形式的に検証した。この手法を水制御システム事例研究で実験的に評価した。時間付きオートマトンへのPLCプログラムの翻訳とモデル検査ツールの使用による検証の以前のアプローチと比較して,著者らのアプローチは,非タイミング関連機能特性を検証するために大幅に拡張可能である。Copyright 2019 The Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 制御系 ,  システム設計 ,  言語 ,  *応用プログラム ,  事例研究 ,  プログラマブルコントローラ ,  モデル検査 ,  突然変異 ,  安全性 ,  コンパイラ
準シソーラス用語： 有界 ,  機能性 ,  設計ツール ,  設計モデル ,  *Simulink , 【Automatic Indexing@JST】

分類 (1件)： 図形・画像処理一般  (JE04010I)

タイトルに関連する用語 (5件)： Simulink ,  設計 ,  PLC ,  モデルベース ,  検証