Master Thesis - Formal Synthesis of Decision-making Controllers for Autonomous Vehicles
Master Thesis Opportunities – Gothenburg, Sweden
Zenuity is a young company originated from the safety leaders of the automotive industry. Our aim is to break new grounds with world-class driver assistance functions and autonomous drive technology. Autonomous driving will be a truly transformative technology re-shaping not only the industry, but also the society forever. With our technological innovations Zenuity is determined to be a lead contributor in the process of enabling such a
Deployment of unsupervised vehicle automation on public roads imposes demanding safety requirements on the correctness of decision-making logics /controller software development process. For some safety requirements, the control software needs to operate with only acceptable failure probability of 10-9 per hour. Achieving such reliability is only possible if one could mathematically prove the correctness of controller w.r.t concrete requirements and assumptions. Formal synthesis (correct-by-construction design) could play a key role to fulfil such demanding requirements.
In practice, most of control systems have a hybrid nature, i.e. consist of continuous dynamics and discrete states. In this thesis, we investigate the possibility of using state of the art control synthesis solution for hybrid system to formally design a safety critical part of our decision-making software.
In this project, the selected candidates are expected to develop an understanding of the core ideas behind formal synthesis, learning how to describe requirements in formal language (linear temporal logics) and implement the synthesis problem in a synthesis tool, e.g. TuLiP. Thesis workers should be able to analyze the synthesized controller, simulate the results and possibly compare their solution with other existing solutions.
The thesis is suitable for two engineering students with background in system control. Good mathematical and programming skills, knowledge of discrete event systems, linear temporal logics and formal methods are meritorious.
Further information and contacts
Final application date: December 15th 2017. Please send in individual applications. If you wish to partner with someone, simply note that in your application.
Planned start: Beginning of 2018, with some flexibility.
Duration: 30 ECTS