The project investigates how maritime regulations, expressed in the domain-specific language Legata, can be transformed into formal correctness properties in the actor-based modeling language Rebeca. This transformation enables the use of formal verification techniques to ensure that autonomous surface vessels comply with safety regulations such as COLREG. The study explores both manual and semi-automated approaches, including the use of large language models (LLMs) with zero-shot and one-shot prompting strategies. By mapping legal clauses into formal logical properties, the research aims to bridge the gap between regulatory descriptions and mathematically verifiable system behavior. The results show that transforming Legata clauses into Rebeca correctness properties is feasible, although the success of the transformation depends on the complexity of the clauses and the capabilities of the underlying model. While LLMs can assist in reducing manual effort and speeding up the transformation process, they are not fully reliable due to issues such as inconsistencies and hallucinations. Therefore, human validation remains necessary. The project contributes with transformation guidelines, insights into the use of LLMs for formal language conversion, and a Rebeca model that can be further developed for verifying the behavior of autonomous maritime systems.
The implementation and source code related to this project are available at the link provided below, where all relevant materials, models, and transformation scripts can be accessed for further exploration and replication of the results.
LINK
Note that this is a fork of LINK.
The full thesis document can be downloaded from the link below. LINK