Verifying Collision Avoidance Behaviours for Unmanned Surface Vehicles using Probabilistic Model Checking

详细信息    查看全文

• 作者：Yu Lu ; Hanlin Niu ^{h.niu@cranfield.ac.uk" class="auth_mail" title="E-mail the corresponding author} ; Al Savvaris ; Antonios Tsourdos
• 关键词：unmanned surface vehicles ; collision avoidance ; probabilistic timed automata ; formal methods ; probabilistic model checking
• 刊名：IFAC-PapersOnLine
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：49
• 期：23
• 页码：127-132
• 全文大小：658 K

文摘

Collision avoidance is an essential safety requirement for unmanned surface vehicles (USVs). Normally, its practical verification is non-trivial, due to the stochastic behaviours of both the USVs and the intruders. This paper presents the probabilistic timed automata (PTAs) based formalism for three collision avoidance behaviours of USVs in uncertain dynamic environments, which are associated with the crossing situation in COLREGs. Steering right, acceleration, and deceleration are considered potential evasive manoeuvres. The state-of-the-art prism model checker is applied to analyse the underlying models. This work provides a framework and practical application of the probabilistic model checking for decision making in collision avoidance for USVs.