PhD position: Formal methods for Programming and Analysis of Robust
Behaviors
of
Autonomous Systems
Supervisors:
LESIRE-CABANIOLS Charles (ONERA/DTIS, Univ. Toulouse, France -- charles
[dot] lesire [at] onera [dot] fr)
GODARY-DÉJEAN Karen (LIRMM, Univ Montpellier-CNRS, France)
Location:
Main location : ONERA, Toulouse, France
Secondary location : LIRMM, Montpellier, France
Duration: 3 years.
The development of autonomous robotic systems involves intelligent
functionalities, such as system control,
data processing, or motion planning. These functionalities are
implemented
in programming environments such
as ROS, which produce complex software architectures, involving several
dozens of processes.
The realization of autonomous missions requires the ability to specify
high-level behaviors, which rely on
functionalities provided by the robotic system, without requiring the
user
to have a detailed understanding of
the deployed processes. These functionalities, or skills [1], provide an
abstraction of the capabilities of the
robotic system. From these capabilities, it is necessary to have tools
for
the specification of higher-level
behaviors, and to establish links between the different levels of
abstraction of the system [4]. The increase in
abstraction is necessary on the one hand to limit the expertise required
for
the programming of a complex
mission. This is particularly necessary when interacting with non-expert
users (e.g. marine biologists or
hydrogeologists). On the other hand, it is also a way to limit the level
of
details of the description of the system
behavior while keeping the information necessary to formalize the
execution
of these behaviors, and to verify
them.
Moreover, this thesis project aims at developing underwater robots for
biodiversity observation. The marine
environment is a challenge for autonomous robotics, for many reasons:
the
control of the robot's movements
in 3D in the aquatic environment; the perception of a complex and
dynamic
environment with sensors that are
often very (too) expensive and/or inaccurate; the difficulty of
communication in the aquatic environment, the
partial ignorance of this environment leading to a difficulty in
modeling
the environment, etc...
In this context, the design of autonomous systems is even more complex.
The
specified behaviors must be
robust to the occurrence of failures on the robotic system (e.g., sensor
failure) or to external events. Moreover,
in critical contexts, it is necessary to provide a priori proofs on the
robust and correct behavior of the robotic
system, and on the success of its mission. This is particularly the case
for
exploration applications in difficult
environments such as underwater, where the environment is complex,
dynamic
and often partially unknown.
Moreover, the use of underwater systems for the observation of marine
biodiversity in fragile and protected
environments imposes specific constraints [2] linked to the obligation
to
respect data collection protocols
specific to the biologists, in order to guarantee data consistency,
while
ensuring the safety of the robot and of
the surrounding ecosystem.
This thesis aims at addressing the problem of specifying and analyzing
behaviors for autonomous systems by
means of formal methods. If these methods are already used to analyze
models
of the system, the originality of
the work proposed in this thesis consists in using formal models as
tools
for programming behaviors, so as to
be able to both execute and analyze these models.
The Petri net formalism will be studied in particular because of its
suitability for the specification of concurrent
behaviors, the possibility of synthesizing executable models, and the
availability of analysis tools. The work
done in this thesis will be based on various works done at LIRMM, on
failure
analysis for submarine missions
[2], on the use of model-checking or formal methods to model robotic
missions [3,4]; and at ONERA, on the
formalization of capabilities by formal models [1], or the definition of
a
mission specification framework by Petri
nets [5]. This work will be applied to the specification of exploration
missions for autonomous underwater
robots, and test campaigns in real environment (lac, pool, sea) will
validate the work done.
The Explore team in LIRMM is interested in mobile robotics, and in
particular in the scientific chain allowing the
control of autonomous missions in complex environments. The main
application
filed is underwater robotics,
for example for the observation of biodiversity [6]. This PhD subject is
in
the continuity of work dealing with the
safety of operation and the definition of complex missions [2,4]. They
must
be completed by a more formal
modeling of the robot's capabilities, and a methodology integrating the
verification steps. The work done at
ONERA [1,5] for autonomous drone applications, brings complementary
aspects
that will allow to result in a
common methodology for the specification and the analysis of autonomous
behaviors.
[1] C. Lesire, D. Doose, C. Grand, "Formalization of Robot Skills with
Descriptive and Operational Models", IROS
2020.
[2] A. Hereau, K. Godary-Dejean, J. Guiochet, C. Robert, T. Claverie, D.
Crestani : "Testing an underwater robot
executing transect missions in Mayotte", TAROS 2020.
[3] R. Sadden-Yagoubi, O. Naud, K. Godary-Dejean, D. Crestani,
"Model-checking precision agriculture logistics:
the case of the differential harvesting", DEDS(30), 2020.
[4] S. Louis, K. Godary-Dejean, L. Lapierre, T. Claverie, S. Villéger,
"Formal method for mission controller
generation of a mobile robot", TAROS 2017.
[5] C. Lesire, F. Pommereau, "ASPiC: an Acting system based on Skill
Petri
net Composition", IROS 2018.
[6] M. Maslin, S. Louis, K. Godary-Dejean, L. Lapierre, S. Villéger, T.
Claverie, "Underwater robots provide similar
fish biodiversity assessments as divers on coral reefs ", under review,
2021.
--
Charles Lesire
Ph.D., HDR
ONERA/DTIS, Toulouse, France
Head of the Safe, Embedded, and Autonomous Systems (SEAS) team
Associated Researcher, ANITI (Artificial and Natural Intelligence
Toulouse Institute)
Visiting Professor, ISAE-Supaero, Toulouse, France
https://sites.google.com/view/charles-lesire
----
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ [email protected] ]]
