  The paper proposes a method for the correct by design coordination of
autonomous driving systems (ADS). It builds on previous results on collision
avoidance policies and the modeling of ADS by combining descriptions of their
static environment in the form of maps, and the dynamic behavior of their
vehicles. An ADS is modeled as a dynamic system involving a set of vehicles
coordinated by a Runtime that based on vehicle positions on a map and their
kinetic attributes, computes free spaces for each vehicle. Vehicles are bounded
to move within the corresponding allocated free spaces. We provide a correct by
design safe control policy for an ADS if its vehicles and the Runtime respect
corresponding assume-guarantee contracts. The result is established by showing
that the composition of assume-guarantee contracts is an inductive invariant
that entails ADS safety. We show that it is practically possible to define
speed control policies for vehicles that comply with their contracts.
Furthermore, we show that traffic rules can be specified in a linear-time
temporal logic, as a class of formulas that constrain vehicle speeds. The main
result is that, given a set of traffic rules, it is possible to derive free
space policies of the Runtime such that the resulting system behavior is safe
by design with respect to the rules.
