On Formal Methods for Design and Verification of Maritime Autonomous Surface Ships

Abstract

Maritime Autonomous Surface Ships (MASS) are approaching a reality, introducing a new level of complexity and criticality to maritime control systems. In this paper we investigate how Formal Methods (FMs) can be used to design and verify maritime control systems for safe and effective MASS. FMs are a family of mathematically based methods for specification and verification. We begin by giving a high-level introduction to FMs. We discuss the current practice for certification of maritime control systems and needs going towards autonomy. We give three specific examples on how FMs can be applied to meet these needs: Formal specification of COLREG, contract-based design and automation of simulation-based testing. Finally, some limitations of FMs are discussed. We conclude that FMs appear as a promising candidate to meet some of the needs going towards autonomy, and encourage further research into FMs for MASS.

On Formal Methods for Design and Verification of Maritime Autonomous Surface Ships