Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems

Fatima Shokri-Manninen; Jüri Vain; Marina Walden

doi:10.1007/978-3-030-58768-0_3

Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems

Fatima Shokri-Manninen, Jüri Vain, Marina Walden

Doctoral Network in Information Technologies and Mathematics

Research output: Chapter in Book/Conference proceeding › Conference contribution › Scientific › peer-review

7 Citations (Scopus)

91 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Software Engineering and Formal Methods
Subtitle of host publication	18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings
Editors	Frank de Boer, Antonio Cerone
Publisher	Springer, Cham
Pages	41-59
Number of pages	19
ISBN (Print)	978-3-030-58767-3
DOIs	https://doi.org/10.1007/978-3-030-58768-0_3
Publication status	Published - 2020
MoE publication type	A4 Article in a conference publication
Event	International Conference on Software Engineering and Formal Methods - SEFM 2020 Duration: 14 Sept 2020 → 18 Sept 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12310 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Software Engineering and Formal Methods
Period	14/09/20 → 18/09/20

Access to Document

10.1007/978-3-030-58768-0_3

SEFM2020_ShoVaWaAccepted author manuscript, 1.32 MBLicence: Publisher rights policy

Cite this

Shokri-Manninen, F., Vain, J., & Walden, M. (2020). Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems. In F. de Boer, & A. Cerone (Eds.), Software Engineering and Formal Methods: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings (pp. 41-59). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12310 LNCS). Springer, Cham. https://doi.org/10.1007/978-3-030-58768-0_3

Shokri-Manninen, Fatima ; Vain, Jüri ; Walden, Marina. / Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems. Software Engineering and Formal Methods: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings. editor / Frank de Boer ; Antonio Cerone. Springer, Cham, 2020. pp. 41-59 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{211f902d857d4398b2d1ec49a828b6af,

title = "Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems",

abstract = "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. ",

author = "Fatima Shokri-Manninen and J{\"u}ri Vain and Marina Walden",

year = "2020",

doi = "10.1007/978-3-030-58768-0_3",

language = "English",

isbn = "978-3-030-58767-3",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Cham",

pages = "41--59",

editor = "{de Boer}, Frank and Antonio Cerone",

booktitle = "Software Engineering and Formal Methods",

note = "International Conference on Software Engineering and Formal Methods ; Conference date: 14-09-2020 Through 18-09-2020",

}

Shokri-Manninen, F, Vain, J & Walden, M 2020, Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems. in F de Boer & A Cerone (eds), Software Engineering and Formal Methods: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12310 LNCS, Springer, Cham, pp. 41-59, International Conference on Software Engineering and Formal Methods, 14/09/20. https://doi.org/10.1007/978-3-030-58768-0_3

Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems. / Shokri-Manninen, Fatima; Vain, Jüri; Walden, Marina.
Software Engineering and Formal Methods: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings. ed. / Frank de Boer; Antonio Cerone. Springer, Cham, 2020. p. 41-59 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12310 LNCS).

Research output: Chapter in Book/Conference proceeding › Conference contribution › Scientific › peer-review

TY - GEN

T1 - Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems

AU - Shokri-Manninen, Fatima

AU - Vain, Jüri

AU - Walden, Marina

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-58768-0_3

DO - 10.1007/978-3-030-58768-0_3

M3 - Conference contribution

SN - 978-3-030-58767-3

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 41

EP - 59

BT - Software Engineering and Formal Methods

A2 - de Boer, Frank

A2 - Cerone, Antonio

PB - Springer, Cham

T2 - International Conference on Software Engineering and Formal Methods

Y2 - 14 September 2020 through 18 September 2020

ER -

Shokri-Manninen F, Vain J, Walden M. Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems. In de Boer F, Cerone A, editors, Software Engineering and Formal Methods: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings. Springer, Cham. 2020. p. 41-59. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-58768-0_3

Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this