| 講演名 | 2017-07-19 端末交通システムにおける運行スケジュールのモデル検査法を用いたデッドロック検出手法 辻 光顕(筑波大), 長谷部 浩二(筑波大), 加藤 和彦(筑波大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 著者らは車両の自律動作により隊列走行可能な端末交通システムの研究開発を行っている．このシステムの特長は，隊列を再編成することにより，旅客の乗り換え動作を排することができる点にある．一方で，隊列の再編成のルールや各車両の運行経路によっては，どの車両も次の停留所に移動できないデッドロックの状態に陥る可能性がある．本論文では，与えられた運行スケジュールにおけるデッドロックの可能性を検出する手法を提案する．特にここではシステムの状態を網羅的に探索するためにモデル検査法を用いる．また，いくつかの具体例をもとに提案手法の有用性を示す． |
| 抄録(英) | The authors are developing a last-mile transportation system with autonomous vehicles. The greatest feature is that passengers do not have to transfer by means of the way of rearrangement of fleets. On the other hand, due to the rules for rearranging fleets and the traveling route of vehicles, any vehicle may fall into a deadlock situation where it cannot proceed to the next stop. To address this problem, in this paper we propose a method to detect the possibility of deadlock in a given operation schedule. For this objective, we use a model checking method to search all possible states of the system. We also demonstrate the usefulness of the proposed method by using some examples. |
| キーワード(和) | デッドロック / 形式手法 / モデル検査法 / 端末交通システム |
| キーワード(英) | Deadlock / Formal Method / Model Checking / Last-Mile Transportation |
| 資料番号 | SS2017-2,KBSE2017-2 |
| 発行日 | 2017-07-12 (SS, KBSE) |
| 研究会情報 | |
| 研究会 | SS / KBSE / IPSJ-SE |
|---|---|
| 開催期間 | 2017/7/19(から3日開催) |
| 開催地（和） | 函館コミュニティプラザ |
| 開催地（英） | |
| テーマ（和） | ソフトウェア工学全般／知能ソフトウェア工学全般／ソフトウェアサイエンス全般 |
| テーマ（英） | |
| 委員長氏名（和） | 緒方 和博(北陸先端大) / 金田 重郎(同志社大) |
| 委員長氏名（英） | Kazuhiro Ogata(JAIST) / Shigeo Kaneda(Doshisha Univ.) |
| 副委員長氏名（和） | 中田 明夫(広島市大) / 粂野 文洋(日本工大) |
| 副委員長氏名（英） | Akio Nakata(Hiroshima City Univ.) / Fumihiro Kumeno(Nippon Inst. of Tech.) |
| 幹事氏名（和） | 小林 隆志(東工大) / 肥後 芳樹(阪大) / 岩田 一(神奈川工科大) / 櫻井 孝平(金沢大) |
| 幹事氏名（英） | Takashi Kobayashi(Tokyo Inst. of Tech.) / Yoshiki Higo(Osaka Univ.) / Hajime Iwata(Kanagawa Inst. of Tech.) / Kohei Sakurai(Kanazawa Univ.) |
| 幹事補佐氏名（和） | 島 和之(広島市大) / 猿渡 卓也(NTTデータ) / 木村 功作(富士通研) |
| 幹事補佐氏名（英） | Kazuyuki Shima(Hiroshima City Univ.) / Takuya Saruwatari(NTT DATA) / Kosaku Kimura(Fujitsu labs.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Software Science / Technical Committee on Knowledge-Based Software Engineering / Special Interest Group on Software Engineering |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 端末交通システムにおける運行スケジュールのモデル検査法を用いたデッドロック検出手法 |
| サブタイトル（和） | |
| タイトル（英） | Deadlock Detection in Scheduling of Last-Mile Transportation by Using Model Checking |
| サブタイトル（和） | |
| キーワード(1)（和/英） | デッドロック / Deadlock |
| キーワード(2)（和/英） | 形式手法 / Formal Method |
| キーワード(3)（和/英） | モデル検査法 / Model Checking |
| キーワード(4)（和/英） | 端末交通システム / Last-Mile Transportation |
| 第 1 著者 氏名（和/英） | 辻 光顕 / Mitsuaki Tsuji |
| 第 1 著者 所属（和/英） | 筑波大学(略称：筑波大) University of Tsukuba(略称：Univ. of Tsukuba) |
| 第 2 著者 氏名（和/英） | 長谷部 浩二 / Koji Hasebe |
| 第 2 著者 所属（和/英） | 筑波大学(略称：筑波大) University of Tsukuba(略称：Univ. of Tsukuba) |
| 第 3 著者 氏名（和/英） | 加藤 和彦 / Kazuhiko Kato |
| 第 3 著者 所属（和/英） | 筑波大学(略称：筑波大) University of Tsukuba(略称：Univ. of Tsukuba) |
| 発表年月日 | 2017-07-19 |
| 資料番号 | SS2017-2,KBSE2017-2 |
| 巻番号（vol） | vol.117 |
| 号番号（no） | SS-136,KBSE-137 |
| ページ範囲 | pp.7-12(SS), pp.7-12(KBSE), |
| ページ数 | 6 |
| 発行日 | 2017-07-12 (SS, KBSE) |