Verification of autonomous underwater vehicles using formal logic

Formal systems verification of autonomous underwater vehicles (AUV) is addressed in this paper. Verification includes hybrid system modelling, discrete abstractions, control systems abstractions, checking of reachability of undesirable states by formal model checking. The main contribution of the paper is to show how first multilayered hybrid system modelling, then its representation and discretisation in Stateflow™, can be automatically compiled into interpreted script (ISPL) of the multi-agent model checker system (MCMAS) for verification. Using this technique, modelling and model checking can include the complete physical system of the autonomous vehicle, its multi-agent software on board and also the human interface represented as an agent.