Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussaKonferenssiartikkeliTieteellinenvertaisarvioitu

Abstrakti

Along with the very actively progressing field of autonomous ground and aerial vehicles, the advent of autonomous vessels has brought up new research and technological problems originating from the specifics of marine navigation. Autonomous ships are expected to navigate safely and avoid collisions following COLREG navigation rules. Trustworthy navigation of autonomous ships presumes applying provably correct navigation algorithms and control strategies. We introduce the notion of maritime game as a special case of Stochastic Priced Timed Game and model the autonomous navigation using UPPAAL STRATEGO. Furthermore, we use the refinement technique to develop a game model in a correct-by-construction manner. The navigation strategy is verified and optimized to achieve the goal to safely reach the manoeuvre target points at a minimum cost. The approach is illustrated with a case study inspired by COLREG Rule 15.
AlkuperäiskieliEnglanti
OtsikkoSoftware Engineering and Formal Methods
Alaotsikko18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings
ToimittajatFrank de Boer, Antonio Cerone
KustantajaSpringer, Cham
Sivut41-59
Sivumäärä19
ISBN (painettu)978-3-030-58767-3
DOI - pysyväislinkit
TilaJulkaistu - 2020
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Conference on Software Engineering and Formal Methods - SEFM 2020
Kesto: 14 syyskuuta 202018 syyskuuta 2020

Julkaisusarja

NimiLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vuosikerta12310 LNCS
ISSN (painettu)0302-9743
ISSN (elektroninen)1611-3349

Konferenssi

KonferenssiInternational Conference on Software Engineering and Formal Methods
Ajanjakso14/09/2018/09/20

Sormenjälki

Sukella tutkimusaiheisiin 'Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Viittausmuodot