文献

J-GLOBAL ID：201702231629371199   整理番号：17A1255007

時間付きオートマトンを用いたROSをベースとしたロボット応用の形式的検証【Powered by NICT】

Formal Verification of ROS-Based Robotic Applications Using Timed-Automata

著者 (4件)： Halder Raju ,  Proenca Jose ,  Macedo Nuno ,  Santos Andre
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： FormaliSE  ページ： 44-50  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： ロボット技術は,家庭用および工業用環境を形質転換した。最近ロボットオペレーティングシステム(ROS)は,産業界及び学界の両方を採用し,ロボットアプリケーションを開発するための最もよく知られたミドルウェア枠組みの一つになりつつされてきた。ロボットシステムの正しい挙動を保証したパラメタリゼーションと不均一性の可能性のために,しかしながら,挑戦的である。異なるアプローチが存在し,特定のシナリオに対する具体的ドメイン空間に焦点を当てたが,ROSシステム推論への一般的なアプローチはまだ求められている。本論文では,実時間特性を用いたROSシステムをモデル化し,検証,ROSの主な特徴,ノード間の通信の一つに焦点を当てアプローチを提案した。低レベルパラメータ,待ち行列サイズとタイムアウトなどを,モデリング言語としての時間付きオートマトンを用いた。ロボットKobukiは複雑な事例研究,特性は,UPPAALモデルチェッカーを用いて検証し,問題パラメータの組合せの同定を可能にするものであるとして使用されている。Copyright 2017 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件)： 図形・画像処理一般  (JE04010I) ,  CAD,CAM  (JE10000A)

タイトルに関連する用語 (5件)： 時間付きオートマトン ,  ROS ,  ロボット ,  応用 ,  形式的検証