System Verification of Autonomous Underwater Vehicles by Model Checking

The paper addresses formal systems verification of autonomous underwater vehicles (AUV). The verification process includes hybrid system modelling and formulation of the discrete representation using natural language programming (sEnglish) via compositional abstraction - employing data, perception and action abstraction methods; the translation of the discrete abstraction into interpreted script programming language (ISPL) of a mainstream multi-agent model checker (MCMAS) for reachability verification of undesirable states, and ultimately the bridging into the discrete event system representation in Stateflow formalism. 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.