Model Checking for Decision Making System of Long Endurance Unmanned Surface Vehicle

TL;DR

This paper develops a model checking approach using Kripke models and MCMAS to verify the decision-making system of a long-endurance USV, ensuring safety and reliability in complex, uncertain environments.

Contribution

It introduces a novel application of model checking to verify USV decision systems considering environmental uncertainties and energy management.

Findings

Verification confirms safety properties of USV decision system

Model checking identifies potential design errors early

Feasibility demonstrated for long-endurance USV scenarios

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.