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.