dc.contributor.author | Smogeli, Øyvind Rasmussen | |
dc.contributor.author | Glomsrud, Jon Arne | |
dc.contributor.author | Utne, Ingrid Bouwer | |
dc.contributor.author | Sørensen, Asgeir Johan | |
dc.date.accessioned | 2023-02-20T10:00:41Z | |
dc.date.available | 2023-02-20T10:00:41Z | |
dc.date.created | 2023-02-13T22:04:50Z | |
dc.date.issued | 2023 | |
dc.identifier.issn | 0029-8018 | |
dc.identifier.uri | https://hdl.handle.net/11250/3052255 | |
dc.description.abstract | 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. | en_US |
dc.language.iso | eng | en_US |
dc.publisher | Elsevier Ltd. | en_US |
dc.rights | Navngivelse 4.0 Internasjonal | * |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/deed.no | * |
dc.title | Towards contract-based verification for autonomous vessels | en_US |
dc.title.alternative | Towards contract-based verification for autonomous vessels | en_US |
dc.type | Peer reviewed | en_US |
dc.type | Journal article | en_US |
dc.description.version | publishedVersion | en_US |
dc.source.volume | 270 | en_US |
dc.source.journal | Ocean Engineering | en_US |
dc.identifier.doi | 10.1016/j.oceaneng.2023.113685 | |
dc.identifier.cristin | 2125800 | |
dc.source.articlenumber | 113685 | en_US |
cristin.ispublished | true | |
cristin.fulltext | original | |
cristin.qualitycode | 1 | |