Formal and risk-based methods for designing, testing and verifying autonomous marine control systems
This presentation will discuss recent research performed at NTNU on formal and risk-based methods applied to autonomous marine systems, introduced by prof. Asgeir J. Sørensen. Thomas will present his work on risk-based control for autonomous surface ships. The work is based on an extended System Theoretic Process Analysis (STPA) that is used to build a Bayesian Belief Network (BBN) risk model. The risk model is used in a supervisory risk controller to set high-level control objectives for the ship control system. Tobias will present his PhD work on using formal methods to design and verify autonomous surface ships. This includes an automated method for simulation-based verification using Signal Temporal Logic and Gaussian Processes and early-stage work on using formal contracts to design modular and verifiable autonomous systems. Renan will present his work on decision-making in Autonomous Marine Vehicles (AMV) based on dynamic risk assessment. A Dynamic Probabilistic Risk Assessment (DPRA) framework was conceived, which uses component-based simulation to identify and quantify all possible accident scenarios in AMV operation. The output from DPRA will then be used for autonomous decision-making – e.g., modifying existing plans to avoid hazardous events.