Towards contract-based verification for autonomous vessels

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.