Formal Development of Multi-vessel Navigation of Maritime Autonomous Systems using UPPAAL

Fatemeh Shokri, Juri Vain, Marina Walden*

*Corresponding author for this work

Research output: Chapter in Book/Conference proceedingConference contributionScientific

Abstract

There is a very actively progressing field of Multi-Agent Systems (MAS), which can be viewed as safety-critical systems. The key reason for applying formal methods to MAS is to ensure the correctness of such a system and bring trust for a wide range of application conditions.
Autonomous ships constitute a class of safety-critical multi-agent systems that have to operate under maritime specific conditions. An autonomous ship should be able to detect other vessels and make appropriate adjustments of speed and course to avoid collisions at the same time maintaining maritime traffic rules. The challenge in this area is the development of a formal modelling and verification technique relevant for the domain specifics. In particular such systems must guarantee safe performance of each agent in the shared environment considering various environment conditions and other agents on the route. One important feature that needs to be particularly addressed in formal modelling of such systems is the agility, efficiency and safety of the ships’ dynamic reaction also to the stochastic behaviour of other agents under extreme circumstances such as drift of ice fields or loss of radio link. In addition to collisions avoidance, agents are expected to reduce fuel consumption for a voyage for cost saving and minimising air pollution.
In our research, we use UPPAAL STRATEGO for verifying and synthesising safe navigation of autonomous ships. As an additional contribution, we improve the multi-vessel navigation quality characteristics regarding its safety and security and with that improving the planning of the optimal route and scheduling manoeuvers according to COLREG rules.
Original languageEnglish
Title of host publicationProceedings of the 32nd Nordic Workshop on Programming Theory
Place of PublicationIceland
PublisherReykjavik University, Iceland
Number of pages4
Publication statusPublished - 2021
MoE publication typeB3 Non-refereed article in conference proceedings
Event32nd Nordic Workshop on Programming Theory - Reykjavik University, Reykjavik, Iceland
Duration: 4 Nov 20216 Nov 2021
http://icetcs.ru.is/nwpt21/

Workshop

Workshop32nd Nordic Workshop on Programming Theory
Country/TerritoryIceland
CityReykjavik
Period04/11/2106/11/21
Internet address

Keywords

  • Verification
  • Maritime Autonomous Systems
  • COLREG rules
  • Collisions Avoidance
  • Multi-vessel Navigation
  • Multi-Agent Systems
  • Safety
  • Optimization

Fingerprint

Dive into the research topics of 'Formal Development of Multi-vessel Navigation of Maritime Autonomous Systems using UPPAAL'. Together they form a unique fingerprint.

Cite this