| 講演名 | 2016-03-11 一次元系における自己位置推定の振舞い検証に向けて 関澤 俊弦(日大), 岡野 浩三(信州大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 組込みシステムが社会に広く普及するに伴い，その信頼性は重要となっている．モデル検査は信頼性保証技術の一つであり，様々なシステムの信頼性を保証するために適用され成功を収めてきた．しかし，確率的な振舞いを示す系への適用は十分とは言い難い．本研究は，自律移動ロボットなどに代表される確率ロボティックスの要素技術の一つである自己位置推定をモデル検査で扱うことを目的とする．そのために，一定の制約を課した1次元系における自己位置推定アルゴリズムのモデル化と検証事例を示す．本研究では，モデル検査の適用可能性を示すために，モデル検査器としてSPIN を使用する． |
| 抄録(英) | Along with the popularization of embedded systems in society, reliability of them has become important. Model checking is one of formal methods which has been successfully applied to many systems for ensuring theirreliabilities. However, applications for probabilistic systems are not yet enough studied. The aim of this study is to establish a self-localization method based on model checking. Self-localization is one of elements of probabilistic robot techniques which involve autonomous mobile robots. This study shows a model representing a self-localization algorithm on one-dimensional system with restrictions, and also the model checking results. This study uses model checker SPIN in order to show applicability of classical model checking approaches. |
| キーワード(和) | 自己位置推定 / 1次元系 / モデル検査 |
| キーワード(英) | estimation of self-localization / one-dimensional system / model checking |
| 資料番号 | SS2015-100 |
| 発行日 | 2016-03-03 (SS) |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2016/3/10(から2日開催) |
| 開催地（和） | 沖縄県立宮古青少年の家 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 委員長氏名（和） | 結縁 祥治(名大) |
| 委員長氏名（英） | Shoji Yuen(Nagoya Univ.) |
| 副委員長氏名（和） | 緒方 和博(北陸先端大) |
| 副委員長氏名（英） | Kazuhiro Ogata(JAIST) |
| 幹事氏名（和） | 小林 隆志(東工大) / 鷲崎 弘宜(早大) |
| 幹事氏名（英） | Takashi Kobayashi(Tokyo Inst. of Tech.) / Hironobu Washizaki(Waseda Univ.) |
| 幹事補佐氏名（和） | 肥後 芳樹(阪大) |
| 幹事補佐氏名（英） | Yoshiki Higo(Osaka Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Software Science |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 一次元系における自己位置推定の振舞い検証に向けて |
| サブタイトル（和） | |
| タイトル（英） | Towards Behavior Verification of Estimation of Self-localization in One-dimensional Systems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 自己位置推定 / estimation of self-localization |
| キーワード(2)（和/英） | 1次元系 / one-dimensional system |
| キーワード(3)（和/英） | モデル検査 / model checking |
| 第 1 著者 氏名（和/英） | 関澤 俊弦 / Toshifusa Sekizawa |
| 第 1 著者 所属（和/英） | 日本大学(略称：日大) Nihon University(略称：Nihon Univ.) |
| 第 2 著者 氏名（和/英） | 岡野 浩三 / Kozo Okano |
| 第 2 著者 所属（和/英） | 信州大学(略称：信州大) Shinshu University(略称：Shinshu Univ.) |
| 発表年月日 | 2016-03-11 |
| 資料番号 | SS2015-100 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | SS-508 |
| ページ範囲 | pp.145-150(SS), |
| ページ数 | 6 |
| 発行日 | 2016-03-03 (SS) |