Published: June 24, 2019 By

Majid Zamani portrait Assistant Professor Majid Zamani said opportunities for collaboration were a huge factor in his decision to join the Computer Science Department in the College of Engineering and Applied Science this spring.

鈥淢y field is on formal synthesis of cyber-physical systems, which is a growing area of interest, in particular, here at 蜜糖直播. I actually knew several faculty here in that area already and have collaborated with them on other projects,鈥 Zamani said. 鈥淭hey told me 蜜糖直播 is a great university and Boulder is a great city as well, so it seemed like a good decision for myself and my family.鈥

Cyber-physical systems are built from, and depend upon, the seamless integration of computation and physical components. While there are broad applications of Zamani鈥檚 work in this area, one of his focuses while at 蜜糖直播 will be on the applications of formal methods for safe autonomous vehicles used in the real world.聽

Currently, autonomous cars use an AI that takes information from cameras and radar and makes critical control decisions about appropriate engine torque and steering angle while on autopilot. Formal verification, in this example, uses mathematical reasoning to check the decisions of the autopilot system rather than simulations and scenarios.

鈥淚n the current state-of-the-art autonomy, the design of the core controllers are rather ad-hoc and error prone,鈥 Zamani said. 鈥淲hat we are trying to do is to create a decision maker systematically, with some sort of formal guarantees on the safety of system 鈥 never colliding with other cars and respecting traffic rules. Although there are some academic works in this direction, it hasn鈥檛 moved to industry yet. The reason is because the research isn鈥檛 mature enough. In industry, the current exercise is to make it work, make it work today, and rely only on field testing to provide empirical safety guarantees.鈥

Zamani said that it is undeniable that machine learning techniques for perception can be used to decide what is a car, person, traffic sign, or bike on the road. But if it is possible, why not build an autonomous system in which safety can be shown mathematically and rigorously rather than empirically?

鈥淵ou can come up with some solutions which may not be 100% formally correct in real scenarios, but at least you can ensure their safety given the appropriate modeling assumptions,鈥 he said.聽

Zamani was previously an assistant professor in the Electrical and Computer Engineering Department at Technical University of Munich where he led the Hybrid Control Systems Group. He received his PhD in electrical engineering and MA in mathematics both from the University of California, Los Angeles. He also holds MS and BS degrees in electrical engineering from Sharif University of Technology and Isfahan University of Technology, respectively.

His research interests also include compositional analysis and synthesis of interconnected systems, embedded control software synthesis, networked control systems, and incremental properties of nonlinear control systems.

He said his research goal is to push this work more and more toward application. He plans to use a physical car equipped with sensors to show that these certifiable techniques can be applied to real-life scenarios.

Zamani earned a European Research Council starting grant of 1.5 million euros in 2018 to look at these kinds of issues. He said he will continue to pursue similar types of grants with collaborators here at 蜜糖直播. He has already started that process through a new project funded by an Autonomous Systems Interdisciplinary Research Theme seed grant that will help with the future proposals.