2024-03-29T20:15:06Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001826802024-03-29T05:26:34Z01164:01384:09129:09211
端末交通システムにおける運行スケジュールのモデル検査法を用いたデッドロック検出手法Deadlock Detection in Scheduling of Last-Mile Transportation by Using Model Checkingjpnhttp://id.nii.ac.jp/1001/00182592/Technical Reporthttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=182680&item_no=1&attribute_id=1&file_no=1Copyright (c) 2017 by the Institute of Electronics, Information and Communication Engineers This SIG report is only available to those in membership of the SIG.筑波大学情報学群情報科学類筑波大学システム情報系情報工学域筑波大学システム情報系情報工学域辻, 光顕長谷部, 浩二加藤, 和彦著者らは車両の自律動作により隊列走行可能な端末交通システムの研究開発を行っている.このシステムの特長は,隊列を再編成することにより,旅客の乗り換え動作を排することができる点にある.一方で,隊列の再編成のルールや各車両の運行経路によっては,どの車両も次の停留所に移動できないデッドロックの状態に陥る可能性がある.本論文では,与えられた運行スケジュールにおけるデッドロックの可能性を検出する手法を提案する.特にここではシステムの状態を網羅的に探索するためにモデル検査法を用いる.また,いくつかの具体例をもとに提案手法の有用性を示す.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.AN10112981研究報告ソフトウェア工学(SE)2017-SE-1962162017-07-122188-88252017-07-07