文献

J-GLOBAL ID：202102232728948316   整理番号：21A0993123

IEC61131-3PLCプログラムのためのユーザフレンドリーな検証アプローチ【JST・京大機械翻訳】

A User-Friendly Verification Approach for IEC 61131-3 PLC Programs

著者 (6件)： Xiong Jiawen (National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, China) ,  Zhu Gang (National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, China) ,  Huang Yanhong (National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, China) ,  Huang Yanhong (Hardware/software Co-Design Technology and Application Engineering Research Center, Shanghai 200062, China) ,  Shi Jianqi (National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, China) ,  Shi Jianqi (Hardware/software Co-Design Technology and Application Engineering Research Center, Shanghai 200062, China)
資料名： Electronics (Web)  (Electronics (Web))
巻： 9  号： 4  ページ： 572  発行年： 2020年 
JST資料番号： U7178A  ISSN： 2079-9292  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： スイス (CHE)  言語： 英語 (EN)

抄録/ポイント： プログラマブル論理コントローラ(PLC)は,産業制御システムで広く使われる特別な組込みコンピュータである。産業制御システムの安全性を確実にするため,PLCsの正当性を検証する必要がある。正式検証は,PLCプログラムがその仕様に適合するかどうかを検証する効果的方法であると考えられているが,専門知識要求と複雑性は,それを習得し,広く適用することを困難にする。本論文では,IEC61131-3PLCプログラムのための仕様マイニングベース検証アプローチを示した。それは,特定の仕様のためのモデル検査の代わりに,プログラム行動からマイニングされた仕様を見直すだけを必要として,それは安全性検証の効率性を大いに改良することができて,使用のための制御システムエンジニアにとって非常に簡単であった。さらに,PLCプログラムからLTL仕様とデータ不変量を直接マイニングするPLCInspectorという概念証明ツールを実装した。2つの例と1つの現実の事例研究を示し,その実用性と効率を説明した。さらに,PLCプログラムに対する既存の検証手法との比較を議論した。Copyright 2021 The Author(s) All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 規格 ,  制御装置 ,  不変量 ,  *事例研究 ,  コンピュータ ,  モデル検査 ,  システムエンジニア
準シソーラス用語： *ユーザフレンドリ性 ,  複雑性 ,  専門知識 , 【Automatic Indexing@JST】

著者キーワード (5件)： IEC611313規格 ,  産業用制御システム ,  PLC ,  仕様マイニング ,  検証

分類 (4件)： システム設計・解析  (IA02030D) ,  計算機システム開発  (JD02010R) ,  電気式制御機器  (IC02020Y) ,  CAD,CAM  (JE10000A)

引用文献 (39件)：

• Chen, G.; Song, X.; Gu, M. PLC program verification and analysis using the Coq theorem prover. ACTA Sci. Nat. Univ. Pekin. 2010, 46.
• Blech, J.O.; Biha, S.O. Verification of PLC properties based on formal semantics in Coq. In Proceedings of the International Conference on Software Engineering and Formal Methods, Montevideo, Uruguay, 14-18 November 2011; pp. 58-73.
• Schlich, B.; Brauer, J.; Wernerus, J.; Kowalewski, S. Direct model checking of PLC programs in IL. IFAC Proc. Vol. 2009, 42, 28-33.
• Pavlovic, O.; Ehrich, H.D. Model checking PLC software written in function block diagram. In Proceedings of the 2010 Third International Conference on Software Testing, Verification and Validation, Paris, France, 7-9 April 2010; pp. 439-448.
• Darvas, D.; Blanco, E.; Fernández Adiego, B. Transforming PLC Programs into Formal Models for Verification Purposes; Technical Report, No. CERN-ACC-NOTE-2013-0040; CERN: Geneva, Switzerland, 2013.

タイトルに関連する用語 (2件)： ユーザフレンドリー ,  検証