Modular assurance of an Autonomous Ferry using Contract-Based Design and Simulation-based Verification Principles

TL;DR

This paper presents a structured framework combining contract-based design and simulation testing to assure the safety of autonomous ferries, specifically focusing on collision avoidance, and providing formal evidence for assurance cases.

Contribution

It introduces the ADA framework for assurance of digital assets and demonstrates its application to an autonomous ferry using simulation and formal methods.

Findings

Successful demonstration of collision avoidance assurance for the ferry

Integration of simulation-based testing with contract-based verification

Framework provides formal evidence for safety assurance

Abstract

With the introduction of autonomous technology into our society, e.g. autonomous shipping, it is important to assess and assure the safety of autonomous systems in a real-world context. Simulation-based testing is a common approach to attempt to verify performance of autonomous systems, but assurance also requires formal evidence. This paper introduces the Assurance of Digital Assets (ADA) framework, a structured method for the assurance of digital assets, i.e. novel, complex, or intelligent systems enabled by digital technologies, using contract-based design. Results are shown for an autonomous ferry assurance case, focusing on collision avoidance during the ferry's transit. Further, we discuss the role of simulation-based testing in verifying compliance to contract specifications, to build the necessary evidence for an assurance case.