文献

J-GLOBAL ID：201802288824644043   整理番号：18A0164428

サイバー物理agnosticソフトウェアのための形式的検証に向けて:事例研究【Powered by NICT】

Towards formal verification for cyber-physically agnostic software: A case study

著者 (4件)： Drozdov Dmitrii (Lulea& University of Tehcnology, Lulea&, Sweden) ,  Patil Sandeep (Lulea& University of Tehcnology, Lulea&, Sweden) ,  Dubinin Victor (Penza State University, Penza, Russian Federation) ,  Vyatkin Valeriy (Lulea& University of Tehcnology, Lulea&, Sweden)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： IECON  ページ： 5509-5514  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： サイバーフィジカルagnosticism(CPA)は種々の外乱に耐えると物理過程の必要な行動を維持する維持するサイバー物理システム(CPS)におけるソフトウエアの特性である。産業オートメーション(IoT A)におけるインターネットの(IoT)の使用に増加した研究によって,そのようなIoT装置における無線デバイスを用いたいくつかのオーバーヘッドを考慮に入れることができるロバストな分散自動化制御システムが必要である。例えば,無線センサとコントローラ間のデータ転送遅延は古いセンサ値に作用するコントローラをもたらす可能性がある。本論文では,IoTの応用のCPA特性をチェックする方法として入力データと形式的検証の品質を評価するためのコントローラに時間を考慮した計算を用いる方法を提示した。特異的に分布したIoTの応用の実現のためのIEC-61499-スタンダードを考察した。Ptolemy II PTIDES触発された時間スタンプ事象意味論は異なる事象の起源の軌跡を保つへの応用に使用されている。時間付きオートマトンは植物をモデル化した。抽象プラントモデルと共にIEC六万千四百九十九の応用は,SMV言語に変換され,NuSMVモデルチェッカは形式的検証に使用されている。本論文では,提案した手法を実証するエレベータ例の事例研究を示した。ランダム遅延を用いて無線ネットワークにおける通信遅延をモデル化した。通信遅延を考慮しなかったならば,エレベータは床を中間停止と不安全な考えられているドアを開くであろうことを示した。,時間を考慮したか計算を用いて,エレベータは常に安全挙動に従うことを確認するためにであることを示した。Copyright 2018 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： 意味論 ,  モデリング ,  センサ ,  インターネット ,  制御装置 ,  *ソフトウェア ,  自動制御 ,  ロバスト性 ,  *事例研究 ,  安全性 ,  データ転送 ,  エレベータ
準シソーラス用語： 通信遅れ ,  モノのインターネット ,  *形式的検証 , 【Automatic Indexing@JST】

分類 (2件)： 計算機網  (JC03000K) ,  通信網  (ND07030A)

タイトルに関連する用語 (4件)： 物理 ,  ソフトウェア ,  形式的検証 ,  研究