Formal Verification of Autonomous Marine Systems
Background & motivation
- Formal Verification (FV) refers to a class of verification methods which use mathematical analysis to establish proofs of correctness of a system. Prominent FV tools include Model Checkers, Theorem Provers and Reachability Analysis.
- FV is attractive as it can produce exhaustive verification results, but it is typically limited to simple systems due to complexity in modelling and the so-called state-space explosion problem.
- FV has traditionally been applied to highly critical systems in applications such as aerospace, nuclear and aviation. Recently there has been increasing interest in applying FV to address some of the verification challenges for autonomous systems.
- There has not been any application of FV to autonomous marine vessels yet. Pioneering work is required to explore possible uses. The thesis will represent a first-take on formal verification of autonomous marine systems.
- The student should perform a literature study on the field of FV and pinpoint relevant methods and uses.
- The student should work with the milliAmpere 2 autonomous passenger ferry as a case study to explore and demonstrate FV of an autonomous system. This includes:
- Selecting a relevant subsystem of milliAmpere 2 and creating a model suitable for FV.
- Formulate formal requirements to verify against, using e.g temporal logic.
- Use FV to verify the correctness of the system against the requirements.
- A possible subsystem to consider is the supervisory controller of milliAmpere 2. This is implemented as a finite-state machine which is responsible for high-level control of the ferry crossing. This includes transitions such as take-off, crossing and docking.
Figure 1: A presentation of different FV tools.