IEEE Robotics & Automation Magazine - September 2011 - 22

FROM THE GUEST EDITORS *

Robot Challenges: Toward Development
of Verification and Synthesis Techniques
van de Molengraft (M.j.G.v.d.Molengraft@tue.nl), Michael Beetz, and Toshio Fukuda
By Rene

obots often fail to do what we
expect them to do; they go
the wrong way, they drive
into obstacles, and sometimes
they just stay in place until we figure
out what went wrong. In the current
design process of robotic systems, especially in the decision making and control algorithms, an engineer designs the
system, tests it, fixes it in case a bug
was found, and
* then tests again,
In synthesis, a correct
until he or she decides that the sysdesign is guaranteed
tem is reliable
to be automatically
enough; if the behavior of the rogenerated from the
bot needs to be
specification.
changed, this time* consuming and
error-prone process
is repeated. How can we improve
this process? How can we guarantee
the correct robot behavior? How can
we ensure that robots will always
be safe?
Formal methods, an important area
in computer science, deal with algorithms and tools for the verification and
synthesis of correct-by-construction
hardware and software systems. For
example, model-checking tools, given
a system model and a specification,
either return an answer that the system
is guaranteed to satisfy the specification or provide a counter example that
depicts run of the system contradicting
the specification. In synthesis, a correct
design is guaranteed to be automatiDigital Object Identifier 10.1109/MRA.2011.942486
Date of publication: 13 September 2011

IEEE ROBOTICS & AUTOMATION MAGAZINE

cally generated from the specification.
This area, which boasts several Turing
Award winning researchers, had great
impact on industries with verification
techniques becoming standard tools in
large companies such as Intel.
Robots, cyber-physical systems that
interact with dynamic environment
and humans, pose unique challenges
for the development of verification and
synthesis techniques. One has to take
into consideration the dynamics of the
robot, sensor and actuation noise,
strict safety considerations, interaction
with nonexpert users, and so on.
This special issue describes the
work being done toward creating
formal methods for robotics and automation. Inherent to the approaches
presented in this special issue is the
idea that a robot, or team of robots,
can be modeled as a hybrid system-a
system that is defined by both discrete
(states/modes) and continuous variables. Each mode can be viewed as a
node in a state machine that has a
dynamics associated with it, typically
a set of differential equations. The
continuous variables evolve based on
the dynamics of the mode in which
the system is in. For example, consider a car driving on a straight road.
The modes might be accelerate, brake,
reverse, and stopped. The continuous
variables might be position or velocity. If the car is in brake mode, then
the velocity variable might be governed by the equation m_ ¼ À1.
Another example of a hybrid system model of robot motion, as
described in some of the articles in
this issue, is based on an abstraction

SEPTEMBER 2011

of the workspace. One can partition
the workspace of the robot into
regions, which are the modes, and design controllers capable of driving the
robot from one region to an adjacent
region. The position of the robot in
the environment dictates the mode of
the hybrid system.
The first three articles of the special
issue rely on the notion of reachability
analysis. Given a set of initial conditions, there are several approaches for
calculating, exactly or approximately,
the set of states that the system might
reach. Reachability analysis can be
used to verify that the system does not
reach a bad set of states, and it can be
used to synthesize control so that the
system is guaranteed to be safe (always
in a good set).
In "Robotic Surgery," the authors
model the control system for robotic
surgery as hybrid automata and use
reachability analysis to verify the safety
of the simple action of puncturing, in
the presence of model uncertainties.
The authors use ARIADNE, a model
checker for nonlinear hybrid automata, to analyze the system with respect to desired timing and force
properties.
In "Hybrid Systems in Robotics,"
the authors compute reachable sets to
derive control laws that ensure that the
robot reaches a desired state while
avoiding a set of bad (unsafe) states.
The article includes three examples: a
quadrotor performing aerobatics maneuvers, a quadrotor remaining in a
safe set while subject to disturbances
and noise, and decision making in a
capture-the-flag game.

Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - September 2011