Project Title:
Methods of reliability
control for AUVs.
Dr Levente
Molnar
Tel: 02380-592873 (ext: 22873)
Email: l.molnar@soton.ac.uk
Objectives of the project:
The ongoing
AUV verification project encompasses the following goals:
(1) Development of a model based
multi-dimensional integrity and fault assessment system (IFAS) for individual design
analysis;
(2) Development of a design optimization
tool for overall operational reliability (DOPTOR) that allows interactive use
by designers;
(3) Development of a system of human
interface for daily operation (HIDO) that relies on IFAS and DOPTOR to provide
a disciplined practical advisory and warning system for the technical staff
handling the vehicle on board a ship or offshore;
This first objective of the project
is obtained by using model checking techniques applied to a suitable model of
the autonomous system. It consists of the following steps:
-
A
formal model is defined for the examined autonomous system, i.e. the Autosub AUV developed by the project’s industrial partner
the Underwater Systems Laboratory of the National Oceanography Centre
Southampton.
-
The
model is refined for adapting it for the chosen mainstream model checker. The
extensive refinement consists in a discrete abstraction of the hybrid system
model and a conversion of the design into a formalism accepted by the model
checking tool.
-
The
requirements of the system are analyzed and stated in collaboration with the
project partner, hence asserting the properties that the design must satisfy.
The specifications to be verified are formulated in the model checker’s logical
formalism.
-
The
model checker is used to verify whether these requirements are satisfied or
whether bugs exist.
-
Feedback
is provided if necessary, for the AUV designers to extend and/or refine the
system.
The second objective proposes the
development of the DOPTOR interactive tool that uses IFAS and that can be used
during assembly and (re-)configuration of the vehicle offshore. It helps to
optimize what IFAS measures, such that in addition to the reliability
measurement carried out by the IFAS, DOPTOR provides the facilities for
iterative changes and evaluation of the AUV. DOPTOR is a sequence of computer
guided and human executed procedures, where computer checks inform humans about
conditions and the next steps to be taken. Real time operational conditions are
derived from the model checking analysis automatically and transmitted to
engineers launching, through hand-held wireless communication devices.
The last objective aims toward the
realization of the human interface for daily operation (HIDO). HIDO is intended
as a system, to be used by technical staffs onboard a ship who may not know
very well the AUV. It can help to keep track of procedures, to solve arising
problems or making decisions, and help to avoid potential hazards. HIDO is a
communication and software system that includes computers and communication
networks between operators to monitor the human steps of AUV handling. HIDO
avoids and guards over human errors made during commissioning, launch and
retrieval, passing instructions to operators in a rigorous manner.
Methods used from
mathematical logic and computer science, context dependent language theory:
- use of natural language programming (see at http://en.wikipedia.org/wiki/natural_language_programming
) ,
- data, perception and action abstraction methods
in engineering
- model checking by MCMAS (model checker for
multi-agent systems) is used for verification of hybrid systems in
engineering
Publications in preparation:
1. L Molnar
and S M Veres (2008). Verification of autonomous vehicle
systems by formal logic. Submitted to European Control Conference,
ECC’09,
2. L Molnar
and S M Veres (2008). System verification of AUVs by model checking. Submitted
to OCEANS ´09 IEEE Bremen: Balancing technology with future needs, 11–14 May
2009,