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.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

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


    Beteiligte:

    Erscheinungsdatum :

    2021-01-01


    Anmerkungen:

    Shokri-Manninen , F , Vain , J & Waldén , M 2021 , ' Formal Development of Multi-vessel Navigation of Maritime Autonomous Systems using UPPAAL STRATEGO ' , 32nd Nordic Workshop on Programming Theory , Reykjavik , Iceland , 04/11/21 - 06/11/21 . < https://urn.fi/URN:NBN:fi-fe2023050139694 >


    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Klassifikation :

    DDC:    629



    Online and Proactive Vehicle Rerouting with Uppaal Stratego

    Bilgram, Alexander / Ernstsen, Emil / Greve, Peter et al. | Transportation Research Record | 2021


    Verification of quasi-synchronous systems with Uppaal

    Bhattacharyya, S. / Miller, S. / Yang, J. et al. | IEEE | 2014


    Verification of quasi-synchronous systems with Uppaal

    Bhattacharyya, Siddhartha Sid | IEEE | 2014


    Maritime Training Serbian Autonomous Vessel Protection Detachment

    Šoškić Svetislav D. / Radojević Slobodan M. / Komazec Nenad M. | DOAJ | 2014

    Freier Zugriff