Safety Certified Cooperative Adaptive Cruise Control under Unreliable
Inter-vehicle Communications*

arXiv:1609.07501v1 [] 23 Sep 2016

Rafael Rodrigues da Silva1,2 and Hai Lin1
Abstract— Cooperative adaptive cruise control(CACC) system provides a great promise to significantly reduce traffic
congestion while maintaining a high level of safety. Recent
years have seen an increase of using formal methods in the
analysis and design of cooperative adaptive cruise control
systems. However, most existing results using formal methods
usually assumed an ideal inter-vehicle communication, which
is far from the real world situation. Hence, we are motivated
to close the gap by explicitly considering non-deterministic
time delay and packet dropout due to unreliable inter-vehicle
communications. In particular, we consider a passive safety
property, which requests a vehicle to avoid any collisions that
can be considered as its fault. Under the assumption that
the communication delay is bounded and we know the upper
bound, we then formally verify the passivity safety of a class
of hybrid CACC systems. This result allows us to define a safe
control envelope that will guide the synthesis of control signals.
Vehicles under the CACC within the safe control envelope are
guaranteed to avoid active collisions.

I. I NTRODUCTION
The road transportation system is crucial to the economic
because it provides a reliable passenger and goods traffic
that moves the domestic and international trade. Hence, the
traffic safety and capacity is of major concern. In the US,
more than 35,000 people died in motor vehicle accidents in
2015 [1]. Moreover, the growing traffic demand in the US is
faster than its expansion and causes an increasing congestion
cost that reached 160 billions of dollars in 2014 [18]. Those
facts are motivating transportation agencies to consider nontraditional solutions such as the Intelligent Transportation
System (ITS) to maximize the traffic throughput of existing
transportation system as reducing the risk of accidents [4].
In particular, Adaptive Cruise Control (ACC) was introduced as a possible solution to those issues. ACC allows a
shorter safe distance to the preceding vehicle by measuring
the vehicle’s relative distance and velocity and adjusting the
speed accordingly. Although radar sensors are adequate to
measure relative distance, to use the wheel speed measurement shared through the network can reduce the uncertainty
inherent in radar measurements and further reduce the safe
distance between vehicles. Thus, a lot of research activities in
ITS have been devoted to the study of Cooperative Adaptive
Cruise Control (CACC) [16], [8], [11], [9], [19], [17], [4]
and the references therein.
*The financial supports from NSF-CNS-1239222, NSF-CNS-1446288
and NSF- EECS-1253488 for this work are greatly acknowledged.
1 All authors are with Department of Electrical Engineering,
University of Notre Dame, Notre Dame, IN 46556, USA.

(rrodri17@nd.edu; hlin1@nd.edu)
2 The first author would like to appreciate the scholarship support by
CAPES/BR, BEX 13242/13-0

CACC systems are ensured through two different approaches: the string stability analysis and hybrid system
verification. The string stability analysis approaches consider the problem of finding a regulator that the vehicle
acceleration, velocity or distance error will not be amplified
for a given headway (i.e. relative distance divided by the
vehicle speed). For example, in [16], the authors proposed a
regulator that considers communication delay and presented
experimental results with a platooning of similarly adapted
vehicles. A regulator with an online uncertainties estimation
was proposed in [19]. A consensus-based approach for a
string stable regulator was proposed in [17] to address both
communication delays and package losses.
The hybrid system verification approaches, on the other
hand, model the CACC system as a hybrid system and
investigate the problem of finding the safe distance between
vehicles. Most existing work along this line assumed an ideal
inter-vehicle communication network, see e.g., [8] and [11].
The package loss was considered in [9], but assumed that it
can find a timeout based on a network model to ensure the
safety by asking for the human assistance. Therefore, a verification approach that considers both communication delay
and package loss without relying on human interventions has
not been considered yet.
Hence, we are motivated to close the gap by explicitly
considering non-deterministic time delay and packet dropout
due to unreliable inter-vehicle communications. In particular,
we aim to verify a passive safety of a control envelope
for CACC systems in differential dynamic logic (dL) for
a highway scenario where each vehicle is equipped with
relative distance and velocity sensors and inter-vehicle communication devices. The passive safety specification requires
that the vehicle should avoid any collision with other vehicles
in which can be considered its fault [10]. A control envelope is a class of control systems which dL could model
and verify [2]. We assume that the communication is not
ideal and is subject to communication delays and package
losses. Since the inter-vehicle communication is an ad-hoc
wireless network where the packages are broadcasted to all
neighboring vehicles, the package loss rate may increase in
noisy environments, and a random delay may also increase
in crowed environments [7], [4].
In summary, our main contribution in this paper lies on
verifying a CACC control envelope to guarantee a passive
safety property for non-ideal communication considering
communication delays and package loss. Furthermore, we
adopt differential cut and weakening dL [14], [15] axioms
to reduce the verification complexity in KeYmaera [13]. To

the best of our knowledge, it has not been attempted before.
• Unlike [16], [19] and [17], in which designed a regulator
that is string stable, this work propose to verify a
safety property for a control envelope. Thus, it ensures collision avoidance for a heterogeneous traffic
scenario because any scenario that the regulators are
in the control envelope will ensure the safety property,
which it could be from semi-autonomous vehicles where
the control systems intervene to avoid collisions to a
fully autonomous vehicle which no human driving is
required.
• Unlike [8] and [11], in which the verification considered
an ideal network, this work considers a more realistic
scenario where the communication is non-ideal and
subject to delays and package loss.
• Unlike [9], in which the safety specification expected
human intervention considering package loss, the control envelope considered in this paper does not require a
human driver to ensure safety under non-deterministic
package losses. Further, in this work, communication
delays is also contemplated.
• Unlike [14] and [15], in which the differential cut and
weakening dL axioms were used to solve undecidable
differential equations, in this work, those axioms were
used to reduce the computational complexity of the
verification in KeYmaera [13]. Since dL verification
is a semi-decidable decision problem [13], a procedure
which reduces the axioms computation complexity can
increase the class of verifiable systems in dL.
The rest of the paper is organized as follows. Section II
presents the scenario and the problem formulation of this
work. Sections III, IV, V, VI and VII describe in details
the verification approach. Finally, Section VIII concludes the
paper.
II. S YSTEM M ODEL AND P ROBLEM F ORMULATION
This work considers a highway scenario illustrated in
Fig. 1, in which it is assumed that all vehicles are equipped
with inter-vehicle wireless network devices. The network can
be ad-hoc, and all vehicles in the highway may broadcast
network packages. Hence, it is assumed that the follower
vehicles are equipped with a localization system that can
distinguish the package from the vehicle immediately in front
of it, i.e. the lead vehicle. Further, the follower vehicles are
equipped with a radar sensor to read the relative distance d
to the lead vehicle. Both vehicles are equipped with sensors
to read their current velocities (i.e. vf and vl , follower and
lead vehicle velocities), and the inter-vehicle network allows
the follower vehicle to receive the readings from lead vehicle
velocity sensor. Finally, the network is not ideal and subject
to communication delays and package losses.
The Fig. 2 shows the delays in this scenario. Th delays
are non-deterministic, and we know bounds. The lead vehicle
will transmit its current velocity periodically with period tl .
We also consider that the control network may introduce a
significant delay td,v , but its maximum value τ is known
(i.e. td,v ≤ τ ). The network receiving period tf is the

Fig. 1.

The local single lane highway scenario considered in this work.

Fig. 2.

The delays considered in the proposed system.

time between lead velocity samples received by the follower
vehicle, and its maximum value  is known and always
greater or equal to maximum communication delay (i.e.
 ≥ τ ). Thus, the follower vehicle can consider that the
current network package is lost if tf > . The td,x is a
delay introduced by the relative distance sensor and is always
smaller than the communication delay (i.e. td,x ≤ td,v ).
The network period tl is greater enough to give time to
the follower vehicle execute its control system tf,comp and
smaller than  − τ (i.e. td,x + tf,comp ≤ tl ≤  − τ ). Thus,
the follower vehicle will receive new lead vehicle velocity
value before or equal  if the network package is not lost.
The follower vehicle control system must guarantee that
it will never actively collide with others vehicles, meaning
that the follower vehicle will never be in an inevitable
active collision state (IaCS) with another vehicle. An IaCS
is an inevitable collision state (ICS) in which the agent is
considered responsible for a collision. ICSs are system states
which no matters the agent does in the future; it will not
avoid the collision [6]. Hence, the ICS is relaxed with some
assumptions which, in this case, are: all vehicles always
drive in the same way (i.e. v ≥ 0), change lane after the
vehicle immediately behind in the other lane yields and
are not responsible for a collision in the back. Hence, the
follower vehicle can collide only if another vehicle enters
in the lane without waiting for the follower vehicle to give
way, is driving in wrong way (v < 0), or collides in the
back of the follower vehicle. It is a fair safe requirement
in a realistic traffic scenario because the traffic performance
is increased assuming that all drivers respect some rules,
including human and machine drivers. Therefore, the system
must ensure a safety property that guarantees ICS-free longitudinal maneuvers between the follower and lead vehicle,
where the lead vehicle is the vehicle immediately in front of
the follower (i.e. always d > 0).
The continuous longitudinal dynamics is modeled by fol-

S

C∧S

III. T HE DL FORMULA φcACC

Drive

Brake

C

S
Fig. 3. Transition system that represents the control envelope to be found
in the proposed problem.

lowing differential equations: x0 = v, v 0 = a, where x, v and
a are the current vehicle position, velocity, and acceleration,
respectively. These equations are considered adequate to
describe longitudinal maneuvers [8], [11], [3], [9]. Hence, the
follower vehicle dynamics is described by x0f = vf , vf0 = af
and the lead vehicle by x0l = vl , vl0 = al . The follower
vehicle acceleration af is changed after receiving a network
package, and the lead vehicle changes its acceleration al
after sending a network package. We assume to know the
maximum realizable braking deceleration B, and it is equal
to both vehicles. We also assume to know the maximum
acceleration A and minimum braking power b of the follower
vehicle.
Instead of finding a unique control system, we propose
to find a control envelope which ensures the safety property
d > 0. A control envelope is a hybrid control system which
represents a class of control systems [2]. Fig. 3 shows this
hybrid control system, where the initial constraint C is a
first-order formula which constraints the states the system
can start and the safe constraint S is a first-order formula
which constraints the states the follower vehicle can drive.
In the case that a vehicle is entering in front of the follower
and at the same lane, a safe give way should respect the
initial constraint C. Being able to drive means that the vehicle
can realize any acceleration a in its domain −B ≤ a ≤ A.
In case that this constraint is not true ¬S, then the vehicle
must brake, i.e. −B ≤ a ≤ −b. Now, we can formulate the
problem.
Problem 1. Given the maximum network receiving period
time  > 0, maximum communication delay τ ≥ 0 ∧  ≥ τ ,
maximum braking deceleration B > 0 for both vehicles,
minimum braking deceleration b > 0 ∧ B ≥ b and maximum
acceleration A > 0 of the follower vehicle; find a control
envelope that guarantees that the follower vehicle will never
actively collide with a vehicle in the proposed highway
scenario.
The approach used in this work to solve the Problem 1
split the verification and design into five steps: design the
dL formula φcACC that specifies the safety requirements,
design the dL hybrid program cACC that models this control
envelope for the proposed cACC, find the loop invariant Cloop
and the initial constraint C for the dL formula, find the safe
constraint S, and the verification of the resulting dL formula
φcACC . In the following sections, we will discuss each one
of those steps.

The Differential Dynamic Logic dL verifies a symbolic
hybrid system model, and, thus, can assist in verifying and
finding symbolic parameters constraints. The iteration between the discrete and continuous dynamics is nontrivial and
leads to nonlinear parameter constraints and nonlinearities in
the dynamics. Most of the time, this turns into an undecidable
problem for model checking [13]. Hence, the model checking
approach must rely on approximations. On the other hand,
the dL uses a deductive verification approach to address
infinite states; it does not rely on finite-state abstractions or
approximations. Thus, a verification in dL can handle those
nonlinear constraints.
The dL formula is a specification language which is a
first-order dynamic logic over the reals for hybrid systems.
Definition 1 (dL formulas). A dL formula [13] (φ and ψ)
is defined as:
φ, ψ ::= χ | ¬φ | φ ∧ ψ | ∀xφ | ∃xφ | [α]φ | hαiφ
where:
• α is a hybrid system modeled as a hybrid program
which is defined in the Sec. IV.
• [α]φ holds true if φ is true after all runs of α.
• hαiφ holds true if φ is true after at least one runs of α.
The safety property proposed in this work is to ensure that
the follower vehicle does not actively collide with another
vehicle in a highway considering the scenario presented in
Sec. II. A collision will occur if the relative distance is zero
(i.e. d = 0), and this distance can be related to the current
position of the lead and follower vehicles (i.e. d = xl − xf ).
Since being a lead vehicle means that lead vehicle position is
always greater and equal to follower position (i.e. xl ≥ xf ),
the safety property which ensures that no collision occurs
is xl − xf > 0. Further, we want ensures that the control
envelope guarantees this property after any non-deterministic
and a finite number of executions. Hence, the following dL
formula φcACC specifies those requirements.
φcACC ≡ C → [(cACC)∗ ](xl − xf > 0)
IV. T HE DL HYBRID PROGRAM cACC
The hybrid systems are embedded to the dL as hybrid programs, a compositional program notation for hybrid systems.
Definition 2 (Hybrid Program). A hybrid program [13] (α
and β) is defined as:
(
x1 := θ1 , ..., xn := θn |?χ | α; β | α ∪ β | α∗ |
α, β ::=
x01 := θ1 , ..., x0n := θn &χ
where:
• x is a state variable and θ a first-order logic term.
• χ is a first-order formula.
• x1 := θ1 , ..., xn := θn are discrete jumps, i.e. instantaneous assignments of values to state variables.

•

•
•
•
•

x01 := θ1 , ..., x0n := θn &χ is a differential equation
system that represents the continuous variation in system dynamics. x0i := θi is the time derivative of state
variable xi , and &χ is the evolution domain.
?χ tests a first-order logic at current state.
α; β is a sequential composition, i.e. the hybrid program
β will start after α finishes.
α ∪ β is a nondeterministic choice.
α∗ is a nondeterministic repetition, which means that α
will repeat for finite times.

The proposed dL hybrid program cACC that models the
control envelope shown in Fig.3 is presented in Model 1. It
is assumed that the control system has a clock tf to detect a
network package loss. This clock counts the maximum time
between the time that the lead velocity was sampled, and
it was received by the follower vehicle. Since the maximum
communication delay τ is known, we know that this clock is
equal to it at receiving event (i.e. tf = τ ). The lead vehicle
velocity received by the follower is the variable vl,d . Thus,
the follower vehicle cannot directly access vl to take its
decisions but only on vl,d , and the safe constraints saf edelay
and saf edrop can only depend on vl,d instead of vl .
Model 1: cACC Hybrid Program
cACC ≡(ctrlf ; dynt ; ctrll ; dyntd )
ctrlf ≡ctrld ∪ ctrlpl ∪ ctrls ∪ ctrlb
ctrld ≡(?((pkgdrop = 0) ∧ (saf edelay ));
tf := τ ; af := ∗; ?(−B ≤ af ≤ A))
ctrlpl ≡(?((pkgdrop = 1) ∧ (saf edrop ));
af := ∗; ?(−B ≤ af ≤ A))
ctrls ≡(?(vf = 0); af := 0)
ctrlb ≡(af := ∗; ?(−B ≤ af ≤ −b))
dynt ≡t := 0; {x0f = vf , vf0 = af , x0l = vl , vl0 = al ,
t0 = 1, t0f = 1&(vf ≥ 0 ∧ vl ≥ 0 ∧ t ≤ )}
ctrll ≡(pkgdrop := 0; vl,d := vl ) ∪ (pkgdrop := 1);
al := ∗; ?(al ≥ −B)
dyntd ≡td := 0; {x0f = vf , vf0 = af ,
x0l = vl , vl0 = al , t0d = 1, t0f = 1
&(vl ≥ 0 ∧ vl ≥ 0 ∧ td ≤ τ ∧ td + t ≤ )}

First, in the hybrid program cACC, the follower vehicle
changes its acceleration af , i.e. executes ctrlf . If it received
a network package (i.e. pkgdrop = 0) and it is safe to drive
considering a network delay (i.e. saf edelay holds true), or it
detected a package loss (i.e. pkgdrop = 1) and is safe even
under this circumstance (i.e. saf edrop holds true); then it can
assign any acceleration in its domain (i.e. ctrld or ctrlpl ).
However, if it receive a network package, it will reset the tf
clock (i.e. tf := τ ). At any moment, the follower vehicle can
brake (i.e. ctrlb ). And it is considered a mode to verify in the

case that the follower vehicle maintain stopped (i.e. ctrls ).
Next, the dynamics dynt models the continuous dynamics
until the lead vehicle changes its acceleration ctrll . The lead
vehicle control system is modeled by a control envelope that
assumes that it can assign any acceleration that is greater than
the maximum braking deceleration (i.e. al ≥ −B) and send
its current velocity (i.e. vl,d := vl ). However, we assume a
network that may be non-deterministically subject to package
loss (i.e. (pkgdrop := 0; vl,d := vl ) ∪ (pkgdrop := 1)).
Finally, the dynamics dyntd models the continuous dynamics
after lead vehicle control cltrl execution and before the
network package receiving or package loss events.
However, the change in the dynamics of the lead vehicle
during the follower cycle time increases the verification
complexity for the KeYmaera. Normally, a verification in
KeYmaera requires solving a real quantifier elimination (QE)
at the end of the proof. Nevertheless, the QE complexity
increases fast on the number of variables [5]. Since the
lead vehicle control cltrl is executed asynchronously with
follower control ctrlf , the number of variables and equations
of the final real QE increases and may not be computable.
Therefore, we propose to augment the Model 1 using Differential Ghosts and Invariants [14] to simplify the final QE
problem. This approach is different from the original purpose
which was to verify systems with undecidable differential
equations without solving them; however, it offers an efficient procedure to simplify dL formulas that lead to complex
QE problems.
The main idea is that QE become simpler for a double integrator system (i.e. x0 = v, v 0 = a) when considering an acceleration that is an equality (e.g. a =
A) instead of an inequality (e.g. −B ≤ a ≤ A).
Thus, it was proposed the following differential ghosts:
0
x0g,f = vg,f , vg,f
= ag,f &vg,f ≥ 0 such that xg,f ≥ xf ∧
0
vg,f ≥ vf , and x0g,l = vg,l , vg,l
= ag,l &vg,l ≥ 0 such that
xg,l ≤ xl ∧ vg,l ≤ vl . Since xg,f ≥ xf ∧ xg,l ≤ xl →
xl − xf ≥ xg,l − xg,f , xg,l − xg,f > 0 → xl − xf >
0. Therefore, introducing these ghosts will turn the proof
simpler for KeYmaera because proving xg,l −xg,f > 0 leads
to a simpler QE problem.
Each control mode in ctrlf should assign an value for ag,f
and ag,l to ensure that xg,f ≥ xf ∧vg,f ≥ vf and xg,l ≤ xl ∧
vg,l ≤ vl . Hence, the ctrld and ctrlpl should assign ag,f = A
and ag,l = −B, the ctrls ag,f = 0 and ag,l = −B and
ctrlb ag,f = −b and ag,l = −B. The resulting augmented
dL hybrid program cACCaug is presented in Model 2. The
augmented dynamic models dynt and dyntd considers when
vg,l = 0 letting it execute with ag,l = 0. Further, the case
when vg,f = 0 is considered because vg,f ≥ vf ∧ vf ≥ 0.
Hence, all reachable states in the hybrid program cACC are
in cACCaug (i.e. JcACCK ∈ JcACCaug K). Therefore, if we
prove φcACC,aug ≡ C → [cACCaug ](xl − xf > 0), then we
prove φcACC (i.e. φcACC,aug → φcACC ).

Model 2: cACCaug Hybrid Program
.
cACCaug ≡(ghostinit ; ctrlf ; dynt ; ctrll ; dyntd )
ghostinit ≡xg,f := xf ; vg,f := vf ; xg,l := xl ; vg,l := vl
ctrlf ≡ctrld ∪ ctrlpl ∪ ctrls ∪ ctrlb
ctrld ≡(?(pkgdrop = 0); tf := τ ; ?(saf edelay ); af := ∗; ?(−B ≤ af ≤ A); ag,f := A; ag,l := −B)
ctrlpl ≡(?(pkgdrop = 1); ?saf edrop ; af := ∗; ?(−B ≤ af ≤ A); ag,f := A; ag,l := −B)
ctrls ≡(?(vf = 0); af := 0; ag,f := 0; ag,l := −B)
ctrlb ≡(af := ∗; ?(−B ≤ af ≤ −b); ag,f := −b; ag,l := −B)
dynt ≡t := 0; dynt,ode ; (?(vg,l = 0; ag,l := 0; dynt,ode ) ∪ (?(vg,l > 0))
0
0
dynt,ode ≡{x0f = vf , vf0 = af , x0l = vl , vl0 = al , x0g,f = vg,f , vg,f
= ag,f , x0g,l = vg,l , vg,l
= ag,l , t0 = 1, t0f = 1

&(vf ≥ 0 ∧ vl ≥ 0 ∧ vg,f ≥ 0 ∧ vg,l ≥ 0 ∧ t ≤ )}
ctrll ≡(pkgdrop := 0; vl,d := vl ) ∪ (pkgdrop := 1); al := ∗; ?(al ≥ −B)
dyntd ≡td := 0; dyntd ,ode ; (?(vg,l = 0; ag,l := 0; dyntd ,ode ) ∪ (?(vg,l > 0))
0
0
dyntd ,ode ≡{x0f = vf , vf0 = af , x0l = vl , vl0 = al , x0g,f = vg,f , vg,f
= ag,f , x0g,l = vg,l , vg,l
= ag,l , t0d = 1, t0f = 1

&(vf ≥ 0 ∧ vl ≥ 0 ∧ vg,f ≥ 0 ∧ vg,l ≥ 0 ∧ td ≤ τ ∧ td + t ≤ )}

V. T HE L OOP I NVARIANT Cloop AND I NITIAL
C ONDITIONS C
The initial constraint C can be divided into two constraints:
parameter constraint Cpar , which constraints the constants
values, and initial state constraint Cini , which assign initial
constraints to variables. The parameter constraint is specified
by the assumptions defined in Sec.II and is Cpar ≡ A >
0∧B > 0∧b > 0∧B ≥ b∧ > 0∧τ ≥ 0∧ ≥ τ . The initial
state constraint Cini depends on the loop invariant Cloop .
The loop invariant Cloop is a first-order formula which
permits to verify non-deterministic repetitions of a hybrid
program (i.e. α∗ ) [13]. It should be initially valid (i.e.
Cpar ∧ Cini → Cloop ) and satisfy the safety property
(i.e. Cloop → xl − xf > 0), and the hybrid program
should preserve it (i.e. Cpar ∧ Cloop → [cACCaug ]Cloop ).
To find it, we use an approach inspired from finding the
controllability constraint presented in [13]. First, it was
found the controllability constraint C¯ which the vehicle
executing ctrlb is able to satisfy the safety property (i.e.
C¯ → [ghostinit ; ctrlb ; dynt ; ctrll ; dyntd ](xf − xf > 0))
because we assume in the control envelope that the follower vehicle must always be able to brake. Next, it was
verified if this constraint is preserved when breaking (i.e.
¯ If so, the loop
C¯ → [ghostinit ; ctrlb ; dynt ; ctrll ; dyntd ]C).
¯ The
invariant should imply this constraint (i.e. Cloop → C).
controllability constraint C¯ found for the hybrid program
cACCaug is C¯ ≡ al ≥ −B ∧ vf ≥ 0 ∧ vl ≥ 0 ∧ xl − xf >
v2

v2

0 ∧ xl − xf > 2bf − 2Bl . It adds another constraint to prove
which is simplified by using the proposed differential ghosts,
2
2
vg,f
vg,l
v2
v2
i.e. xg,l − xg,f > 2b
− 2B
→ xl − xf > 2bf − 2Bl because
vg,f ≥ vf ∧ vg,l ≤ vl ∧ vg,l ≥ 0 ∧ vf ≥ 0 →
2
vg,f
2b

−

2
vg,l
2B .

vf2
2b

−

vl2
2B

≤

The initial state constraint Cini must take in account that
vl is not direct accessible by the follower vehicle system;
¯
thus, it cannot be equal to controllability constraint Cini 6= C.
However, vl,d depends on vl because we know the maximum
delay τ and maximum deceleration B, and a constraint can
be found to imply the controllability constraint (i.e. Cini →
¯ Hence, since vl,d ≥ 0 and vl,d − B · τ ≤ vl , vl,d ≥
C).
v2
(v −B·τ )2 
B ·τ ∧xl −xf > 2bf − l,d 2B
∨ vl,d < B ·τ ∧xl −xf >
2
2 
vf
vf
vl2
2b → xl − xf > 2b − 2B . If the package drop initially, it
assumed that the current vl,d is zero. Thus,
Cini ≡al ≥ −B ∧ vf ≥ 0 ∧ vl ≥ 0 ∧ tf ≥ τ ∧ xl − xf > 0∧
h
pkgdrop = 0 ∧ vl,d − B · τ ≤ vl ∧ vl,d ≥ 0
vf2
(vl,d − B · τ )2
−
)
2b
2B
vf2 
∨ (vl,d < B · τ ∧ xl − xf >
) ∨
2b

vf2 i
pkgdrop = 1 ∧ vl,d = 0 ∧ xl − xf >
2b
Adding the premises about vl,d , the loop invariant that
¯ is,
implies the controllability constraint (i.e. Cloop → C)
∧ (vl,d ≥ B · τ ∧ xl − xf >

Cloop ≡al ≥ −B ∧ vf ≥ 0 ∧ vl ≥ 0 ∧ tf ≥ τ ∧
vf2
v2
vl,d ≥ 0 ∧ xl − xf > 0 ∧ xl − xf >
− l ∧
2b 2B
(pkgdrop = 0 ∧ vl,d − B · τ ≤ vl )∨

(pkgdrop = 1 ∧ vl,d − B · tf ≤ vl )
VI. T HE S AFE C ONDITION S
In the hybrid programs cACC and cACCaug the drive
mode presented in the control envelope (see Fig. 3) was

divided into two modes: drive under communication delay ctrld and drive under package loss ctrlpl . Hence, the
resulting safe constraint is S ≡ saf edelay ∨ saf edrop ,
and it is possible to find them separately. Again, it was
used an approach inspired by finding reactivity in [13].
Therefore, we found the reactivity constraint for driving
under communication delay saf edelay such that Cpar ∧
Cloop → [ghostinit ; ctrld ; dynt ; ctrll ; dyntd ]Cloop is valid
and for driving under package loss saf edrop such that Cpar ∧
Cloop → [ghostinit ; ctrlpl ; dynt ; ctrll ; dyntd ]Cloop is valid. It
was found the same reactivity constraint found in previous


v2
v2
works [8] (i.e. xl − xf > 2bf − 2Bl + Ab + 1 A2 2 + vf );
however, it is assumed that the follower vehicle only access
vl through the variable vl,d , and the following constraints
consider the assumptions about vl,d .

vf2
(vl,d − B · τ )2
−
saf edelay ≡ vl,d ≥ B · τ ∧ xl − xf >
2b
2B
 A 2

A
+
+1
 + vf ∨
b
2

vf2
vl,d < B · τ ∧ xl − xf >
2b
 A 2

A
+
+1
 + vf
b
2

vf2
(vl,d − B · tf )2
saf edrop ≡ vl,d ≥ B · tf ∧ xl − xf >
−
2b
2B
 A 2

A
+
+1
 + vf ∨
b
2

vf2
vl,d < B · tf ∧ xl − xf >
2b
 A 2

A
+1
 + vf
+
b
2
VII. V ERIFICATION OF φcACC
The approach applied to verify the formula φcACC,aug
uses differential invariants and weakening axioms [14], [15].
A differential invariant D is a first-order formula which
represents properties of differential equations using an inductive technique. The differential invariant axiom states that
D is a differential invariant with respect to a differential
equation ν 0 = f (ν), where ν is the set of state variables
in the system, if it is initially true (i.e. P → D, where
P is a set of premises), and its derivative D0 is valid (i.e.
P → ∀ν(D0 |ν 0 =f (ν) )). The differential weakening is a dL
axiom which internalizes that differential equations cannot
leave their domain and differential invariants. This approach
was originally used to solve differential equations which
are not solvable [12]. However, even though the differential equations in cACCaug are solvable in the differential
dynamic logic, these solutions have equations that are not
used in the proof and lack equations directly related to
the properties that are needed to be proven. Therefore,
the proposed approach solves as much as possible these
properties using the differential invariants.
To prove the formula φcACC,aug , the differential equations in the hybrid program cACCaug must prove that it
preserves the loop invariant (i.e. φloop ≡ Cpar ∧ Cloop →

[cACCaug ]Cloop ). To reduce the number of premises at the
final QE problem, the goal is that the last the differential
weakening must be able to generate all premises necessary
to prove φloop .
Hence, for each differential equation system in the hybrid program cACCaug , we apply differential cut and differential invariant axioms until it proves that the hybrid
program preserves the loop invariant Cloop after applying
differential weakening axiom. Differential equation systems in this hybrid program form three logical sequences:
vg,l >0
vg,l >0
ρ1 = {dynt,ode −−−−→ dyntd ,ode −−−−→ ∗}, ρ2 =
vg,l >0

vg,l =0

{dynt,ode −−−−→ dyntd ,ode −−−−→ dyntd ,ode } and ρ3 =
vg,l =0

vg,l =0

{dynt,ode −−−−→ dynt,ode → dyntd ,ode −−−−→ dyntd ,ode }.
Thus, four differential invariants are designed: Dt,1 for
dynt,ode , Dt,2 for dynt,ode after vl,g = 0 in ρ3 , Dtd ,1 for
dyntd ,ode after vg,l > 0 in ρ1 and ρ2 , and Dtd ,2 for dyntd ,ode
after vl,g = 0 in ρ2 and ρ3 .
First, each constraint in Cloop is analyzed to find the
differential invariants. The constraint al ≥ −B can be
proven without a reasoning on the differential equations. The
constraint vf ≥ 0∧vl ≥ 0 can be proven using the differential
equations domain. The constraint tf ≥ τ and vl,d ≥ 0 are
differential invariants in all differential equations because is
initially true and its differential is valid (i.e. (tf ≥ τ )0 ≡
1 ≥ 0 and (vl,d ≥ 0)0 ≡ 0 ≥ 0 are valid). The constraint
Bvl,d ≡ (pkgdrop = 0 ∧ vl,d − B · τ ≤ vl ) ∨ (pkgdrop =
1 ∧ vl,d − B · tf ≤ vl ) is not a differential invariant because
the derivative is not valid (i.e. (vl,d −B·τ ≤ vl )0 ≡ (0 ≥ al )).
However, the constraint B̄vl,d ≡ (pkgdrop = 0 ∧ vl,d − B ·
td ≤ vl ) ∨ (pkgdrop = 1 ∧ vl,d − B · tf ≤ vl ) is invariant
for dyntd ,ode if vl,d − B · tf ≤ vl is initially true. In fact, this
constraint is invariant for dynt,ode and, consequently, initially
true for dyntd ,ode . Moreover, the constraint B̄vl,d implies
Bvl,d (i.e. B̄vl,d → Bvl,d ) because td ≤ τ . The constraint
v2

v2

xl − xf > 0 ∧ xl − xf > 2bf − 2Bl is not invariant for
any differential equation. Nonetheless, it can be proven by
using the proposed differential ghosts as discussed in Sec. IV
and V. Thus, the differential invariants that helps to prove
this constraint is the constraints Bg ≡ vf ≤ vg,f ∧ vl ≥
(0)
vg,l ∧ xf ≤ xg,f ∧ xl ≥ xg,l and Bg ≡ vf ≤ vg,f ∧ xf ≤
xg,f ∧ xl ≥ xg,l after vg,l = 0 because vl ≥ vg,l is not
invariant in this situation, but true because vl ≥ 0. Further,
we will need the solution for the differential ghosts variables
2
Bg,f (t) ≡ vg,f = vf,0 +ag,f ·t∧xg,f = xf,0 +vf,0 ·t+ag,f · t2 ,
2
Bg,l (t) ≡ vg,l = vl,0 +ag,l ·t∧xg,l = xl,0 +vl,0 ·t+ag,l · t2 and
v2

(0)

l,0
Bg,l ≡ vg,l = 0∧xg,l = xl,0 + 2B
after vg,l = 0, where vf,0 ,
vl,0 , xf,0 and xl,0 are the respective state variables values at
beginning of the hybrid program. Therefore, the resulting
differential invariants are:

Dt,1 ≡t ≥ 0 ∧ tf ≥ τ ∧ vl,d ≥ 0 ∧ vl,d − B · tf ≤ vl ∧
Bg ∧ Bg,f (t) ∧ Bg,l (t)
Dt,2 ≡t ≥ 0 ∧ tf ≥ τ ∧ vl,d ≥ 0 ∧ vl,d − B · tf ≤ vl ∧
(0)

Bg(0) ∧ Bg,f (t) ∧ Bg,l

S

Dtd ,1 ≡t + td ≥ 0 ∧ tf ≥ τ ∧ vl,d ≥ 0 ∧ B̄vl,d ∧
Bg ∧ Bg,f (t + td ) ∧ Bg,l (t + td )
Dtd ,2 ≡t + td ≥ 0 ∧ tf ≥ τ ∧ B̄vl,d ∧
(0)

Bg(0) ∧ Bg,f (t + td ) ∧ Bg,l .
Since ag,l = −B in all control modes, the equations
Bg,f (t + td ) and Bg,l (t + td ) imply Bloop,1 ≡ xg,l − xg,f >
2
0 ↔ xl,0 − xf,0 > (ag,f · (t+t2d ) + (t + td ) · vf,0 ) −
2
(vl,0 · (t + td ) − B · (t+t2d ) ) and Bloop,2 ≡ xg,l − xg,f >
2
2
2
2
vg,f
vg,l
vf,0
vl,0
ag,f
2b −2 2B ↔ xl,0 − xf,0 > 2b − 2B + ( b + 1)(ag,f ·
(t+td )
+ (t + td ) · vf,0 ). Further, the equations Bg,f (t + td )
2
(0)
(0)
and Bg,l imply Bloop,1 ≡ xg,l − xg,f > 0 ↔ xl,0 − xf,0 >
2
2
vl,0
(ag,f · (t+t2d ) + (t + td ) · vf,0 ) − 2B
) and Bloop,2 . The

resulting QE problems using the proposed differential ghost
were found decidable in KeYmaera. On the other hand,
if we do not use those ghosts, then we would have more
complex constraints such as vl = vl,0 + al,0 · t + al,1 · td
which depends on two different accelerations: the initial
lead vehicle acceleration al,0 ≥ −B and the acceleration
after ctrll al,1 ≥ −B. Those complex equations may turn
the QE problem not computable. Therefore, the dL formula
φcACC,aug is valid (and can be proved using KeYmaera [13]
with computable QE problems, and it proves φcACC ).
Theorem 1. If the maximum network receiving period time
 > 0, maximum communication delay τ ≥ 0 ∧ τ ≤ ,
maximum braking deceleration B > 0 for both vehicles,
minimum braking deceleration b > 0 ∧ B ≥ b and maximum
acceleration A > 0 of the follower vehicle are known, then
the control envelope shown
in Fig. 3 with constraints
S ≡


pkgdrop = 0 ∧ saf ed ∨ pkgdrop = 1 ∧ saf epl and C ≡
Cpar ∧ Cini modeled by the hybrid program cACC presented
in Model 1 will never lead the follower vehicle to actively
collide with another vehicle. The KeYmaera proof file may
be downloaded from https://notredame.box.com/
s/pc6zt6lx9tet16yyijdsaelzyqkpjt98.
Example 1. A fully autonomous can be a regulator that
accelerates until it reaches the maximum velocity of the
road V and, then, keeps this velocity. This regulator can
be designed using any approach that assigns values to
longitudinal acceleration a that respects the constraints in
the verified control envelope of the Theorem 1. A simple
example assigns values a∗ for the longitudinal acceleration
such as,


A, if S ∧ vf < V
a∗ = 0,
if S ∧ vf = V


−b, otherwise
Example 2. Another example is control system that respects
the constraints in the verified control envelope of the Theorem 1 is a semi-autonomous CACC system that assists
a human drive such that the human is free to accelerate
the vehicle when the constraint S holds true (i.e. M anual
driving). Otherwise, the controller take control of the vehicle

C∧S

Auto

Manual

C

S
Fig. 4. Transition system that represents the control envelope to be found
in the proposed problem.

and stops it (i.e. Auto driving). This control system is
illustrated as a transition system in Fig. 4.
VIII. C ONCLUSION
In this paper, we proposed a safe control envelope for
a realistic traffic scenario where communication delays and
package loss may occur. Thus, any vehicle with a CACC
system in the proposed control envelope is formally proven to
avoid collisions with other vehicles which it can be blamed.
It means that a collision can occur only in the back, or if
the other enters the lane without waiting for a give way or
drives in the wrong way. A fully self-driving vehicle as an
autonomous vehicle which the human is allowed to drive
and the machine intervenes only in unsafe states can be
implemented using a CACC represented by this control envelope. Hence, the result presented here can take into account
a heterogeneous traffic system. Moreover, the robustness to
communication delays and package loss can address ad-hoc
wireless network systems which each vehicle broadcast its
packages. In such network systems, a random delay may be
introduced to increase transmission success rate in a crowed
environment. Thus, the impact of such delay to the safe
distance can help to find tradeoffs between communication
and control performances. Therefore, the CACC presented
in this work is formally proven safe for a realistic traffic
scenario.
In future work, we will implement a control system that
uses this safe control envelope in simulated and real traffic
scenarios.
R EFERENCES
[1] Traffic safety factsresearch note 2015. Technical Report DOT HS
812 318, National Highway Traffic Safety Administration (NHTSA),
August 2016.
[2] Nikos Aréchiga and Bruce Krogh. Using verified control envelopes for
safe controller design. In 2014 American Control Conference, pages
2918–2923. IEEE, 2014.
[3] Nikos Aréchiga, Sarah M Loos, André Platzer, and Bruce H Krogh.
Using theorem provers to guarantee closed-loop system properties. In
American Control Conference (ACC), 2012, pages 3573–3580. IEEE,
2012.
[4] Kakan C Dey, Li Yan, Xujie Wang, Yue Wang, Haiying Shen, Mashrur
Chowdhury, Lei Yu, Chenxi Qiu, and Vivekgautham Soundararaj. A
review of communication, driver characteristics, and controls aspects
of cooperative adaptive cruise control (cacc). IEEE Transactions on
Intelligent Transportation Systems, 17(2):491–509, 2016.
[5] Matthew England and James H Davenport. The complexity of
cylindrical algebraic decomposition with respect to polynomial degree.
arXiv preprint arXiv:1605.02494, 2016.
[6] Thierry Fraichard and Hajime Asama. Inevitable collision statesa step
towards safer robots? Advanced Robotics, 18(10):1001–1024, 2004.

[7] Yong He, Jie Sun, Xiaojun Ma, Athanasios V Vasilakos, Ruixi Yuan,
and Weibo Gong. Semi-random backoff: towards resource reservation
for channel access in wireless lans. IEEE/ACM Transactions on
Networking (TON), 21(1):204–217, 2013.
[8] Sarah M Loos, André Platzer, and Ligia Nistor. Adaptive cruise control: Hybrid, distributed, and now formally verified. In International
Symposium on Formal Methods, pages 42–56. Springer, 2011.
[9] Sarah M Loos, David Witmer, Peter Steenkiste, and André Platzer.
Efficiency analysis of formally verified adaptive cruise controllers.
In 16th International IEEE Conference on Intelligent Transportation
Systems (ITSC 2013), pages 1565–1570. IEEE, 2013.
[10] Kristijan Macek, Dizan Alejandro Vasquez Govea, Thierry Fraichard,
and Roland Siegwart. Towards safe vehicle navigation in dynamic
urban scenarios. Automatika, 2009.
[11] Stefan Mitsch, Sarah M Loos, and André Platzer. Towards formal
verification of freeway traffic control. In Proceedings of the 2012
IEEE/ACM Third International Conference on Cyber-Physical Systems, pages 171–180. IEEE Computer Society, 2012.
[12] André Platzer. Differential dynamic logics-automated theorem proving
for hybrid systems. PhD thesis, Universität Oldenburg, 2008.
[13] André Platzer. Logical analysis of hybrid systems: proving theorems
for complex dynamics. Springer Science & Business Media, 2010.
[14] Andre Platzer. The structure of differential invariants and differential
cut elimination. Logical Methods in Computer Science, 8(4):1–38,
2012.
[15] André Platzer. A uniform substitution calculus for differential dynamic
logic. In International Conference on Automated Deduction, pages
467–481. Springer, 2015.
[16] Jeroen Ploeg, Bart TM Scheepers, Ellen van Nunen, Nathan van de
Wouw, and Henk Nijmeijer. Design and experimental evaluation of
cooperative adaptive cruise control. In 2011 14th International IEEE
Conference on Intelligent Transportation Systems (ITSC), pages 260–
265. IEEE, 2011.
[17] S Santini, A Salvi, AS Valente, A Pescape, M Segata, and R Lo Cigno.
A consensus-based approach for platooning with inter-vehicular communications. In 2015 IEEE Conference on Computer Communications
(INFOCOM), pages 1158–1166. IEEE, 2015.
[18] David Schrank, Bill Eisele, Tim Lomax, and Jim Bak. Urban mobility
scorecard. College Station: Texas A&M Transportation Institute and
INRIX, 2015.
[19] Willem van Willigen, Leon Kester, Ellen van Nunen, and Evert
Haasdijk. Safety in the face of uncertainty. International journal
of intelligent transportation systems research, 13(2):95–106, 2015.

