文献

J-GLOBAL ID：202002283236422271   整理番号：20A1863489

モデル検査による自律車輪ローダの形式的検証【JST・京大機械翻訳】

Formal verification of an autonomous wheel loader by model checking

著者 (4件)： Gu Rong (Maelardalen University, Vaesteras, Sweden) ,  Marinescu Raluca (Maelardalen University, Vaesteras, Sweden) ,  Seceleanu Cristina (Maelardalen University, Vaesteras, Sweden) ,  Lundqvist Kristina (Maelardalen University, Vaesteras, Sweden)
資料名： ACM Proceedings  (ACM Proceedings)
号： FormaliSE ’18  ページ： 74-83  発行年： 2018年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 生産性と労働者の安全を増加させる試みにおいて,建設業は,様々な建設機械が人間介入なしで運転する自律建設現場に向けて移動している。それらのタスクを自律的に実行するために,機械は位置局在化,人間および障害物検出,衝突回避などの異なる特徴を備えている。このようなシステムは,安全限界であり,非常に高い信頼性(例えば,タスクデッドラインの会議,全コストの回避(ファット)事故など)で自律的に動作しなければならない。自律Wheel負荷装置は,キャブの人間なしで建設現場内に材料を輸送する機械である。ローダの信頼性をチェックするために,本論文では,ローダをナビゲートするために使用される抽象化経路計画と衝突回避アルゴリズムを含む,車両制御システムの時間オートマトン記述を提供し,著者らは,様々な機能,タイミング,および安全性要求に対して,UPAALにおける符号化をチェックする。ナビゲーションアルゴリズムの複雑な性質は,ローダの抽象モデリングと検証を非常に困難にする。本研究は,徹底的検証技術が自律システムの開発に早期に適用でき,後に発見された場合,コスト増加を招く可能性のある設計誤差を見つけることができることを示す。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  建設業 ,  信頼性 ,  建設機械 ,  *積込み機械 ,  労働者 ,  自律系 ,  時間制限 ,  *モデル検査 ,  衝突回避 ,  経路探索
準シソーラス用語： 自律性 ,  高信頼性 ,  時間付きオートマトン ,  建設現場 , 【Automatic Indexing@JST】

著者キーワード (6件)： UPPAAL ,  自律車両 ,  衝突回避 ,  形式的検証 ,  モデル検査 ,  時間付きオートマトン

分類 (2件)： 積込機械  (QE03040P) ,  鉱山機械  (QE04000E)

タイトルに関連する用語 (5件)： モデル検査 ,  自律 ,  車輪 ,  ローダ ,  形式的検証