During the last years, automated driving techniques are increasingly capturing the market and gaining visibility for consumers. However, for those (partly) automated cars already driving on the worlds’ roads, system failures are not uncommon and even human fatalties have been reported every now and then.

With Multi-lane Spatial Logic (MLSL), a formal approach was introduced to logically reason about the safety of traffic situations on multi-lane motorways and on country roads. Safety (collision freedom) of an informally specified lane change controller for highways and of an overtaking protocol for country roads was proven.

A major part of this thesis is to develop an extension of MLSL to deal with urban traffic scenarios, thereby focusing on safety aspects of crossing manoeuvres at intersections. To this end, we modify the existing abstract model by introducing a generic topology of urban traffic networks and a crossing controller for turn manoeuvres at intersections. Further on, we define automotive-controlling timed automata, which serve as a formal semantics not only for our crossing controller, but also for the other hitherto informal lane change and overtaking controller. We show that even at intersections we can use purely spatial reasoning, detached from the underlying car dynamics, to prove safety of the crossing controller.

As a second part, we examine desirable properties of the MLSL controllers. While the previous approaches, as well as the first part of this thesis, focus on the important safety property, we now examine liveness of the controllers with an implementation in UPPAAL. Liveness means that something good, e.g. a lane change manoeuvre, finally happens. We also take a glance at a solution to implement fairness into the controllers, e.g. how to implement that no car has to wait unreasonably long in front of an intersection.

Finally, we introduce a case study, where we adapt the MLSL approach to a hazard warning communication protocol. With assistance of UPPAAL, we show that with our protocol, a hazard warning message is delivered timely.