## Proofs for Traffic Safety - a Purely Spatial ApproachDue to the increasing use of automated car controllers, mathematical correct formalisms are needed to describe these controllers and verify their safety. Typical approaches refer to the dynamical behaviour of cars via differential equations. In this way, spatial aspects of cars, like the current position and the space needed for safe braking in case of emergencies, are only available indirectly. However, for the verification of safety properties, e.g., collision freedom, these properties are of inherent importance.In this work we want to simplify safety proofs by abstracting away from the concrete dynamics of cars. Within proofs, explicit assumptions about the behaviour of cars have to be used. These assumptions, e.g. that cars are able to calculate their braking distance, can then be instantiated with more detailed approaches. The contributions of this work are divided into three parts. We present an abstract model of traffic on multi-lane highways which hides the dynamics and only considers a local neighbourhood of each car. Subsequently, we define and analyse a modal logic based on this model to specify and verify safety properties of highway traffic. Finally, we present the application of this logic by formally proving that with a small set of controller restrictions, collisions are avoided. |
||