文献

J-GLOBAL ID：202102227666436056   整理番号：21A0080361

形式的検証とスケジューリング可能性解析の間のギャップの橋渡し:ロボットの事例【JST・京大機械翻訳】

Bridging the gap between formal verification and schedulability analysis: The case of robotics

著者 (2件)： Foughali Mohammed (Universite Grenoble Alpes, CNRS, VERIMAG, Grenoble, France) ,  Hladik Pierre-Emmanuel (LAAS-CNRS, Universite de Toulouse, CNRS, Toulouse, France)
資料名： Journal of Systems Architecture  (Journal of Systems Architecture)
巻： 111  ページ： Null  発行年： 2020年 
JST資料番号： A0883A  ISSN： 1383-7621  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： ロボットと自律車両の展開の課題は,ロボット工学,リアルタイムシステムおよび形式的手法コミュニティ間のギャップを埋める更なる努力を要求する。実際,ロボットがコストのかかるミッションと人間との接触にますます関与しているので,様々なリアルタイム制約の存在におけるそれらの挙動の厳密な形式的検証が重要である。その結果における信頼を増すために,そのような検証は現実にできるだけ近いモデルに関して実行されるべきであり,ロボットプラットフォームとスケジューリング政策によって提供されるコアの数のようなハードウェアとOSの特異性を考慮に入れる。本論文では,動的優先度スケジューラを用いてロボット仕様の時間オートマトンモデルを拡張することができる,新しいバイナリ探索インスパイア技術を提案した。多くのコアを与えられた場合,拡張モデルは,同じモデル検査フレームワークの中で,スケジュール可能性を含む様々な実時間および行動特性に対してチェックできる。本技法はロボットフレームワークからUPPAALへの自動翻訳で実装され,実際のロボット事例研究で評価され,そこでは,文献で使用される計数技術とは対照的にスケーラビリティの大きな利得を示す。Copyright 2021 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 機械翻訳 ,  *スケジューリング ,  *ロボット ,  コミュニティ ,  計数法 ,  実時間処理 ,  ハードウェア ,  利得 ,  事例研究 ,  モデル検査 ,  優先度
準シソーラス用語： ロボット工学 ,  *形式的検証 ,  スケジューラ ,  実時間 , 【Automatic Indexing@JST】

著者キーワード (4件)： 形式的方法 ,  スケジュール可能性解析 ,  ロボット工学 ,  二分探索

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (6件)： 形式的検証 ,  スケジューリング ,  可能性 ,  解析 ,  ギャップ ,  ロボット