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

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.