@InProceedings{ChanM17:CDC,
  author       = {Nicole Chan and Sayan Mitra},
  title        = {Verified hybrid LQ control for autonomous spacecraft rendezvous},
  booktitle    = {IEEE International Conference on Decision and Control (CDC`17)},
  year         = {2017},
  abstract     = {Rendezvous is a fundamental maneuver in autonomous space operations in which an active chaser spacecraft is required to navigate safely to the proximity of a second passive target spacecraft. Ensuring safety of such control maneuvers is challenging and design errors can be expensive. We present the first verified control solution to a benchmark formulation of spacecraft autonomous rendezvous in the form of a hybrid LQR controller verified using a data-driven algorithm. Our hybrid LQR scheme is motivated by enforcing safety constraints rather than optimizing performance, and the control law is formulated by periodically solving optimization problems that depend on the current state. The resulting hybrid system presents a challenge for existing automated formal verification tools due to its lack of a closed-form model description. We overcome this challenge by using a data-driven approach (implemented in the new verification tool DryVR). DryVR relies on simulation traces to compute reachable states of the system over bounded time horizon and initial conditions to rigorously verify that the system does not violate any safety requirements.},
  keywords     = {Aerospace systems},
  pdfslidesurl = {research/presentations/2017/CDC-2017.pdf},
  pdfurl       = {research/2017/0Chan_paper.pdf},
  url          = {https://ieeexplore.ieee.org/document/8263854/},
}
{FanQM:IEEEDT2018,
	title = {Data-driven formal reasoning and their applications in safety analysis of vehicle autonomy features},
	author = {Chuchu Fan and Bolun Qi and  Sayan Mitra}
	journal = {IEEE Design & Test},
	year = {2018},
	month = {January}
	abstract = {Safety analysis of Autonomous Vehicles and Advanced Driver Assist Systems (ADAS) is a central challenge facing the automotive industry. In this paper, we present a recently developed data-driven formal verification technique and demonstrate its applicability in a case study involving integrated safety analysis of an Automatic Emergency Braking (AEB) system. Our technique combines model-based, hybrid system reachability analysis with sensitivity analysis of components with possibly unknown or inaccessible models. The scenarios we consider for safety analysis are representative of the most common type of rear-end crashes, which are used for evaluating AEB and forward collision avoidance systems. We show that our verification tool DryVR can effectively establish safety of these scenarios (specified by parameters like braking profiles, initial velocities, uncertainties in position and reaction times), and compute the severity of accidents for unsafe scenarios. The analysis can quantify the safety envelope of the system in the parameter space which is valuable for both design and certification. We also show how the reachability analysis can be combined with statistical information about the parameters, to assess the risk-level of the system, which in turn is essential, for determining Automotive Safety Integrity Levels (ASIL) mandated by the ISO26262 standard.},
	publisher = {IEEE},
	 Keywords                 = {Automotive systems},
	url = {http://ieeexplore.ieee.org/document/8272345/},
	pdfurl = {research/2018/ASIL_IEEESDT2018.pdf}		 	
}