Formal Verification of the Autosub Autonomous Underwater Vehicle: a Case Study
Levente Molnár, Jonathan Ezekiel, Sándor M. Veres, Alessio R. Lomuscio, Miles Pebody · ePrints Soton (University of Southampton) · 2010
The present document is a case study describing the formal verification of the Autosub Autonomous Underwater Vehicle (AUV).Section II provides a description of the Autosub AUV multi-agent system model.Section III details the specifications that were formulated to verify various requirements and properties of the Autosub model.Appendix I presents the Stateflow diagrams containing the labelled transition system formulation of the multi-agent model.Appendix II provides a listing of the Autosub multi-agent model formulated in the interpreted system programming language (ISPL) input language of the MCMAS model checker for multi-agent systems.Appendix III details the output listing of the verification property results as provided by the MCMAS model checker. II. DESCRIPTION OF THE MULTI-AGENT SYSTEM ISPL MODELThe Human ISPL agent illustrates the functionality of the HT SC human tracking and supervisory control.After vehicle launch and prior to safe recovery, the human operator from the support ship will closely observe the AUV during its operation.When the AUV is within range of the ship, short range telemetry is used to monitor the vehicle systems and transmit surfacing commands.During the mission the vehicle can exceed the short range or acoustic telemetry range such that no information of the vehicle systems or location is available.If the vehicle does not return to the support ship or to a predetermined rendezvous location for recovery as that would be determined by the mission control program and mission configuration parameters during normal/correct operation, an acoustic beacon is lowered from the support ship to trigger the vehicle's onboard homing system.The Human agent implements this model behaviour, such that while the human observes the correct AUV operation it does not take any action, but when the AUV appears faulty the Human agent triggers the homing system with lowering the homing beacon.The MissionScriptExecution ISPL agent models the state machine functionality of the mission control process that is being executed in the Mission Control node [1], [2],