Opponent: Associate Prof. Necmiye Özay, University of Michigan, USA
Examiner: Professor Martin Fabian, Chalmers
Abstract of thesis
One goal of
developing automated road vehicles is to completely free people from driving
tasks. Automated vehicles with no human driver must handle all traffic
situations that human drivers are expected to handle, possibly more. Though
human drivers cause a lot of traffic accidents, they still have a very low
accident and failure rate that automated vehicles must match.
Tactical
planners are responsible for making discrete decisions for the coming seconds
or minutes. As with all subsystems in an automated vehicle, these planners need
to be supported with a credible and convincing argument of their correctness. The
planners interact with other road users in a feedback loop, so their
correctness depends on their behavior in relation to other drivers and road
users over time. One way to ascertain their correctness is to test the vehicles
in real traffic. But to be sufficiently certain that a tactical planner is
safe, it has to be tested on 255 million miles with no accidents.
Formal
methods can, in
contrast to testing, mathematically prove that given requirements are
fulfilled. Hence, these methods are a promising alternative for making credible
arguments for tactical planners’ correctness. The topic of this thesis is the
use of formal methods in the automotive industry to design safe tactical
planners. What is interesting is both how automotive systems can be modeled in
formal frameworks, and how formal methods can be used practically within the
automotive development process.
The main
findings of this thesis are that it is viable to formally express desired
properties of tactical planners, and to use formal methods to prove their
correctness. However, the difficulty to anticipate and inspect the interaction
of several desired properties is found to be an obstacle. Model Checking,
Reactive Synthesis, and Supervisory Control Theory have been used in the design
and development process of tactical planners, and these methods have their
benefits, depending on the application. To be feasible and useful, these
methods need to operate on both a high and a low level of abstraction, and this
thesis contributes an automatic abstraction method that bridges this divide.
It is also
found that artifacts from formal methods tools may be used to convincingly
argue that a realization of a tactical planner is safe, and that such an
argument puts formal requirements on the vehicle’s other subsystems and its
surroundings.
Please note that this thesis may not be copied, distributed or forwarded without prior further permission from the author.
