View source for SURF 2015: Provably-correct control synthesis for automotive active safety systems

'''[[SURF 2015|2015 SURF]] project description'''
*Mentor: [[http:web.eecs.umich.edu/~necmiye|Necmiye Ozay]] (U. Michigan)

'''Note''': This project will be located at the University of Michigan.  It is open only to Caltech students.

A plethora of driver convenience and safety automation systems are being introduced into production vehicles, such as electronic stability control, adaptive cruise control, lane keeping, and obstacle avoidance [1]. Assuring the seamless and safe integration of each new automation function with existing control functions is a major challenge for vehicle manufacturers. In this project we will investigate the use of correct-by-construction control protocol synthesis techniques [2,3,4,5] in automotive active safety systems in order to facilitate easy development and deployment of new automated car safety features.

Correct-by-construction control synthesis combines ideas from computer science and control theory and provides a principled, model-based means for control design. The main workflow in correct-by-construction control synthesis is as follows. One starts with a mathematical model of the system dynamics (usually expressed as ordinary differential equations) and a set of system requirements and assumptions (formally captured via a temporal logic formula). A finite-state approximation of the continuous dynamics is computed. This approximation, namely abstraction, is usually based on partitioning of the state-space while constructing low-level controllers that can regulate the system state between partitions. Then, a discrete synthesis problem is solved to obtain a discrete strategy using ideas from two-player discrete games. This discrete strategy is implemented on the continuous system together with low level controllers. There are software toolboxes (see for instance TuLiP [6], and PESSOA [7]) that implement all of these steps. The focus in this project is to develop new abstraction techniques that can handle delays and uncertainties, two common challenges in car safety applications. 

In particular, the student working on this project will be involved in the following tasks:
-- Developing novel abstraction techniques (incremental and randomized) and investigating possibility of parallel implementations
-- Comparing new and existing abstraction techniques on an adaptive cruise control example (there might also be a possibility of implementing these controllers on the scale car we have in our lab)

Required skills: Some programming experience in Matlab or Python. Linear Algebra. Familiarity with or willingness to learn some mathematical optimization, parallel programming, propositional/temporal logics and automata theory (at the level of first few lectures in [5]) is desired.

[1] NHTSA, “Preliminary Statement of Policy Concerning Automated Vehicles”, 2013. 
[2] P. Nilsson, O. Hussien, Y. Chen, A. Balkan, M. Rungger, A. D. Ames, J. W. Grizzle, N. Ozay, H. Peng, and P. Tabuada, “Preliminary Results on Correct-by-Construction Control Software Synthesis for Adaptive Cruise Control”, IEEE Conference on Decision and Control, 2014. http://web.eecs.umich.edu/~necmiye/n+_cdc14.html
[3] P. Nilsson, and N. Ozay, “Incremental Synthesis of Switching Protocols via Abstraction Refinement”, IEEE Conference on Decision and Control, 2014. http://web.eecs.umich.edu/~necmiye/no_cdc14.html
[4] J. Liu, and N. Ozay, “Abstraction, Discretization, and Robustness in Temporal Logic Control of Dynamical Systems”, International Conference on Hybrid Systems: Computation and Control, 2014. http://web.eecs.umich.edu/~necmiye/lo_hscc14.html
[5] EECI, "Specification, Design, and Verification of Distributed Embedded Systems" course website http://www.cds.caltech.edu/~murray/wiki/index.php/HYCON-EECI,_Spring_2013
[6] T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R.M. Murray, "TuLiP: a software toolbox for receding horizon temporal logic planning", International Conference on Hybrid Systems: Computation and Control, 2011 (software available at http://tulip-control.org/)
[7] M. Mazo Jr., A. Davitian, and P. Tabuada, "PESSOA: A tool for embedded control software synthesis", UCLA Technical Report, 2009 (software available at https://sites.google.com/a/cyphylab.ee.ucla.edu/pessoa/)