Formalizing Testing of Collision Avoidance Systems using Signal Temporal Logic

The development of Maritime Autonomous Surface Ships (MASS) necessitates the integration of intelligent automated systems, which requires comprehensive testing methodologies to ensure their capability and reliability. Simulation-based testing is an important tool for collecting evidence for validating the safety and reliability of Collision Avoidance (COLAV) systems, ensuring safe navigation.
The International Regulations for Preventing Collisions at Sea (COLREG) provide a set of rules applicable to all ships to prevent collision at sea, including remotely operated or autonomous ships. A significant challenge lies in transforming these formal, highly human-centric, requirements into machine-readable acceptance criteria for efficient testing. This study explores formulating the COLREG rules using Signal Temporal Logic (STL) to create an evaluation framework tailored for simulation-based testing.
The paper presents STL formulations of COLREG rules 2, 6, 8, 13, 14, 15, 16 and 17, with a particular emphasis on rule 17, which outlines the actions for the stand-on vessel. Rule 17 mandates that the stand-on vessel maintains its course and speed unless a collision becomes imminent, necessitating evasive action. The proposed approach offers a structured method for the automatic verification of COLAV systems against established international standards. In a simulation of one situation, it is demonstrated how STL can be utilized to verify the compliance and effectiveness of collision avoidance algorithms in safety-critical situations.

Keywords: COLREG, Collision avoidance, Autonomy, Evaluation, Signal temporal logic, Simulation-based testing.