IEEE Robotics & Automation Magazine - September 2011 - 30

Approximate R(W, t), F(W, t), and D(R(W, t)) on the
grid, using the correct approximation type.
- If computing an outer approximation, put the newly
reached cells of F(W, t) and D(R(W, t)) in W.
- If computing an e-lower approximation and the
diameter of F(W, t) is smaller than e, add F(W, t)
to W. Otherwise, do nothing.
- If computing an e-lower approximation and the
diameter of D(R(W, t)) is smaller than e, add
D(R(W, t)) to W. Otherwise, do nothing.
3) Repeat recursively until w is empty or no new cells can
be found.
The output of the reachability routine converges to the best
possible approximations (in the sense defined in [9]) when
the size of the grid, the integration step, and the value of e
converge to zero. Termination of the algorithm is guaranteed even for systems that diverge, by providing a bound on
the evolution time (for finite-time reachability) or on the
state space of the system (for infinite-time reachability).
Outer approximations are used to formally prove that a
system respects a safety property u, as discussed in the
"Formal Verification of Hybrid Automata" section. However,
if an outer approximation of the reachable set does not respect
the safety property, then we cannot say anything about the
safety of the system: it could be the case that the system is safe,
but unsafe behaviors have been included in O because of
overapproximation errors. To prove that a system does not
respect a property in a formal way, an underapproximation of
the reachable set is needed. Unfortunately, in most cases it is
not possible to compute such an underapproximation, or the
only possible underapproximation is the empty set (this is the
case, for instance, of single point and trajectory). To overcome
this problem and establish when a system does not respect a
safety property in a sufficiently large class of practical applications, we use e-lower approximations instead. Let u be a
safety property and X0 be an initial set. If Le is a lowerapproximation of ReachSetH (X0 ) and there exists a point
x 2 Le with distance from SatðuÞ larger than e, we can conclude that there exists at least one point of ReachSetH (X0 )
that lies outside Sat(u), implying that the system is unsafe.
In line of principle, it could be the case that we are
unable to prove or disprove a given property, no matter
how accurate the approximations are. However, this
usually happens for badly modeled systems that are close
to instability. Hence, for reasonable control and mechanical designs, an answer is eventually obtainable. In practice,
since the increase in computation time is exponential in
the number of refinement iterations, the amount of time
required to reach a definite answer could become unaffordable. In this case, it is advisable to modify the system
parameters or simplify the model.
l

Formal Verification of the Case Study
In this section, we show how the verification capabilities of
Ariadne can be applied to our test case. To focus on the
verification part without entering into the robotics details,
30

IEEE ROBOTICS & AUTOMATION MAGAZINE

SEPTEMBER 2011

we assume that an inner controller has been designed in
such a way that the variables in the operational space can
be described by a set of second-order linear differential
equations [22]. Moreover, we consider a simplified version
of the model given in Figure 4, where only the Slow and
Perp locations are present.
In free motion (location Slow), the robot and proportional-derivative controller are expressed by
Ms €x ¼ u,
_ þ Ks (xd À x),
u ¼ Ms €xd þ Ds (x_ d À x)
where (Ms , Ds , Ks ) are the mass-damping-stiffness matrices
describing the controlled robot, x the position/orientation
of the end effector, and xd the reference trajectory.
When the end effector touches the patient, the automaton switches to location Perp. An external force control loop
is activated to guarantee a safe value for the applied force in
terms of both absolute value and orientation. The impedance controller and environment are then modeled by
_ þ Ks (xd À x) þ Kf Ke (x À xe ),
u ¼ ÀMs €xd þ Ds (x_ d À x)
where Ke is the stiffness matrix describing the tissue, Kf the
proportional gain of the force loop, and xe the end effector
position when the patient is touched for the first time.
The reference trajectory in free motion considers only
the x, z and / variables, representing the position and orientation of the end effector on the (x, z) plane; the remaining variables are kept constant. The reference trajectory xd
starts in x0 ¼ 0, zo ¼ 0, and /0 ¼ p=2, with zero velocity,
and should end in xf ¼ 1, zf ¼ 0:2, and /f ¼ 0 after 5 s
following a polynomial trajectory.
The patient is assumed to lie on a plane, with the
unknown target position in the range ½xe À dx , xe þ dx ,
where dx is the uncertainty and xe ¼ 0:95 is the nominal
position. This is formally modeled by pairing an invariant
x xe þ dx in location Slow with a guard x ! xe À dx on
the transition from Slow to Perp. In this way, the transition
can be activated anywhere in the range ½xe À dx , xe þ dx .
In the first step of this verification example, we determine
the values of dx for which the task is feasible in 5 s: that is,
after 5 s of evolution, the location must be Perp, / ¼ 0, and
z 2 ½0:185, 0:195. The procedure starts from a range of
possible values for dx , ½dmin , dmax ¼ ½0, 0:06. This range is
then refined by bisection: at each step, Ariadne computes an
outer approximation O of ReachSetH (X0 , 5:0 s) for
d ¼ (dmin þdmax )=2. If O respects the desired conditions on
/ and z, then d is a safe value for the uncertainty and the
next range for dx is ½d, dmax . Otherwise, d is a possibly
unsafe value and the next range for dx is ½dmin , d. The
procedure stops when jdmin À dmax j is under a threshold of
acceptable precision given by the user.
Figure 6, left column, shows the outer approximation
computed by Ariadne for d ¼ 0:03, projected on the (x, t),
(z, t), and (/, t) planes, respectively. The yellow areas on

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