Model checking for decision making system of long endurance unmanned surface vehicle

Niu, Hanlin, Ji, Ze ORCID: https://orcid.org/0000-0002-8968-9902, Savvaris, Al, Tsourdos, Antonios and Carrasco, Joaquin 2021. Model checking for decision making system of long endurance unmanned surface vehicle. Presented at: 2021 IEEE/SICE International Symposium on System Integration (SII), Iwaki, Fukushima, Japan, 11-14 January 2021. 2021 IEEE/SICE International Symposium on System Integration (SII). IEEE, pp. 256-262. 10.1109/IEEECONF49454.2021.9382677

Preview

PDF - Accepted Post-Print Version Download (1MB) | Preview

Abstract

This work aims to develop a model checking method to verify the decision making system of Unmanned Surface Vehicle (USV) in a long range surveillance mission. The scenario in this work was captured from a long endurance USV surveillance mission using C-Enduro, an USV manufactured by ASV Ltd. The C-Enduro USV may encounter multiple non-deterministic and concurrent problems including lost communication signals, collision risk and malfunction. The vehicle is designed to utilise multiple energy sources from solar panel, wind turbine and diesel generator. The energy state can be affected by the solar irradiance condition, wind condition, states of the diesel generator, sea current condition and states of the USV. In this research, the states and the interactive relations between environmental uncertainties, sensors, USV energy system, USV and Ground Control Station (GCS) decision making systems are abstracted and modelled successfully using Kripke models. The desirable properties to be verified are expressed using temporal logic statement and finally the safety properties and the long endurance properties are verified using the model checker MCMAS, a model checker for multi-agent systems. The verification results are analyzed and show the feasibility of applying model checking method to retrospect the desirable property of the USV decision making system. This method could assist researcher to identify potential design error of decision making system in advance.

Item Type:	Conference or Workshop Item (Paper)
Date Type:	Published Online
Status:	Published
Schools:	Engineering
Additional Information:	"© 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works."
Publisher:	IEEE
ISBN:	9781728176581
ISSN:	2474-2325
Date of First Compliant Deposit:	27 March 2021
Date of Acceptance:	5 October 2020
Last Modified:	09 Nov 2022 10:38
URI:	https://orca.cardiff.ac.uk/id/eprint/140141

Actions (repository staff only)

Edit Item