  One of the challenges in designing safe, reliable and trustworthy Autonomous
Vehicles (AVs) is to ensure that the AVs abide by traffic rules. For this, the
AVs need to be able to understand and reason about traffic rules. In previous
work, we introduce the spatial traffic logic USL-TR to allow for the
unambiguous, machine-readable, formalisation of traffic rules. This is only the
first step towards autonomous traffic agents that verifiably follow traffic
rules. In this research preview, we focus on two further steps: a) retrieving
behaviour diagrams directly from traffic rules and b) converting the behaviour
diagrams into timed automata that are using formulae of USL-TR in guards and
invariants. With this, we have a formal representation for traffic rules and
can move towards the establishment of a Digital Highway Code. We briefly
envision further steps which include adding environment and agent models to the
timed automata to finally implement and verify these traffic rule models using
a selection of formal verification tools.
