*Result*: Towards Hazard Analysis Result Verification for Autonomous Ships: A Formal Verification Method Based on Timed Automata.

*Enhancing the safety standards of autonomous ships is a shared objective of all stakeholders involved in the maritime industry. Since the existing hazard analysis work for autonomous ships often exhibits a degree of subjectivity, in the absence of data support, the verification of hazard analysis results has become increasingly challenging. In this study, a formal verification method in a risk-based assessment framework is proposed to verify the hazard analysis results for autonomous ships. To satisfy the characteristics of high time sensitivity, time automata are adopted as a formal language while model checking based on the formal verification tool UPPAAL is used to complete the automatic verification of the liveness of system modeling and correctness of hazard analysis results derived from extended System-Theoretic Process Analysis (STPA) by traversing the finite state space of the system. The effectiveness of the proposed method is demonstrated through a case study involving a remotely controlled ship. The results indicate that the timed automata network model for remotely controlled ships, based on the control structure, has no deadlocks and operates correctly, which demonstrates its practicability and effectiveness. By leveraging the verification of risk analysis results based on model checking, the framework enhances the precision and traceability of these inputs into RBAT. The results disclose the significance of the collaborative work between safety and system engineering in the development of autonomous systems under the definition of human–computer interaction mode transformation. These findings also hold reference value for other intelligent systems with potential hazards. [ABSTRACT FROM AUTHOR]

Copyright of Journal of Marine Science & Engineering is the property of MDPI and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)*