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

Fatima Shokri-Manninen, Jüri Vain, Marina Waldén*

*Corresponding author for this work

Research output: Contribution to conferenceAbstractScientific

46 Downloads (Pure)


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
Number of pages4
Publication statusPublished - 2021
MoE publication typeO2 Other
Event32nd Nordic Workshop on Programming Theory - Reykjavik University, Reykjavik, Iceland
Duration: 4 Nov 20216 Nov 2021


Workshop32nd Nordic Workshop on Programming Theory
Internet address


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


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

Cite this