Towards contract-based verification for autonomous vessels
Peer reviewed, Journal article
Published version
Permanent lenke
https://hdl.handle.net/11250/3052255Utgivelsesdato
2023Metadata
Vis full innførselSamlinger
Originalversjon
10.1016/j.oceaneng.2023.113685Sammendrag
Design and verification of autonomous vessels represent a major interdisciplinary engineering challenge due to the combination of high system complexity and the interaction with dynamic, uncertain, and unstructured environments. This paper investigates the use of contract-based methods to address both design and verification challenges of control systems for autonomous vessels. The paper first presents a formal framework for specification of components and assume-guarantee contracts using the syntax of the Z3 automated theorem prover. Then, the paper proposes a methodology for contract-based verification using the formal framework. The methodology is divided into 4 steps: (1) Hazard identification between the autonomous vessel and the operative environment in order to define the top-level component and contract, (2) stepwise refinement of the top-level component into detailed sub-components and contracts, (3) definition of test setups for simulation-based testing to verify that components meet their contract, and (4) applying a recursive procedure for contracts-based system verification. The framework and methodology are demonstrated the in a case study with an autonomous passenger ferry.