Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



+44 (0)20 7594 8414a.lomuscio Website




569Huxley BuildingSouth Kensington Campus






BibTex format

author = {Ezekiel, J and Lomuscio, A and Molnar, L and Veres, S and Pebody, M},
doi = {978-1-57735-516-8/IJCAI11-279},
pages = {1659--1664},
title = {Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle},
url = {},
year = {2011}

RIS format (EndNote, RefMan)

AB - We report the results obtained during the verification of Autosub6000, an autonomous underwater vehicle used for deep oceanic exploration. Our starting point is the Simulink/Matlab engineering model of the submarine, which is discretised by a compiler into a representation suitable for model checking. We assess the ability of the vehicle to function under degraded conditions by injecting faults automatically into the discretised model. The resulting system is analysed by means of the model checker MCMAS, and conclusions are drawn on the system's ability to withstand faults and to perform self-diagnosis and recovery. We present lessons learnt from this and suggest a general method for verifying autonomous vehicles.
AU - Ezekiel,J
AU - Lomuscio,A
AU - Molnar,L
AU - Veres,S
AU - Pebody,M
DO - 978-1-57735-516-8/IJCAI11-279
EP - 1664
PY - 2011///
SN - 1045-0823
SP - 1659
TI - Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle
UR -
ER -