Formal verification of an autonomous vehicle control system by the timed OTS/CafeOBJ method

• Item type: SIG Technical Reports(1)
• 公開日: 2023-07-17
• タイトル: Formal verification of an autonomous vehicle control system by the timed OTS/CafeOBJ method
• タイトル / 言語: en
• タイトル: Formal verification of an autonomous vehicle control system by the timed OTS/CafeOBJ method
• 言語: eng
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: Toyama Prefectural University
• 著者所属: Toyama Prefectural University
• 著者所属: Toyama Prefectural University
• 著者所属: Toyama Prefectural University
• 著者所属(英): en
• 著者所属(英): Toyama Prefectural University
• 著者所属(英): en
• 著者所属(英): Toyama Prefectural University
• 著者所属(英): en
• 著者所属(英): Toyama Prefectural University
• 著者所属(英): en
• 著者所属(英): Toyama Prefectural University
• 著者名: Masaki, Nakamura; Tatsuya, Igarashi; Yifan, Wang; Kazutoshi, Sakakibara
• 著者名(英): Masaki, Nakamura; Tatsuya, Igarashi; Yifan, Wang; Kazutoshi, Sakakibara
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: The Lim-Jeong-Park-Lee protocol (LJPL protocol) has been proposed as an efficient distributed mutual exclusion algorithm for intersection traffic control, which manages a queue of vehicles to enter the intersection. In our previous work, we have verified its safety property by using the timed OTS/CafeOBJ method in a macro level. In this study, we model an autonomous vehicle control system of the queue as a micro level of LJPL protocol, where a vehicle can enter the intersection even if the vehicle in front is still crossing it under some time constraints. We describe a formal specification of the model and verify its safety property by the timed OTS/CafeOBJ method.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: The Lim-Jeong-Park-Lee protocol (LJPL protocol) has been proposed as an efficient distributed mutual exclusion algorithm for intersection traffic control, which manages a queue of vehicles to enter the intersection. In our previous work, we have verified its safety property by using the timed OTS/CafeOBJ method in a macro level. In this study, we model an autonomous vehicle control system of the queue as a micro level of LJPL protocol, where a vehicle can enter the intersection even if the vehicle in front is still crossing it under some time constraints. We describe a formal specification of the model and verify its safety property by the timed OTS/CafeOBJ method.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10505667
• 書誌情報: 研究報告数理モデル化と問題解決（MPS）; 巻 2023-MPS-144, 号 7, p. 1-4, 発行日 2023-07-17
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8833
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会