Tutorial 16 | 7th Jan | 14:00PM-17:00PM (IST)
Cerifiable Autonomous Cyber-Physical System Design
Speakers: Prof. Samarjit Chakrabarty, UNCChapel Hill; Prof. Sridhar Duggirala, UNC Chapel Hill and Prof. Indranil Saha, IIT Kanpur
About Speakers:
Prof. Samarjit Chakraborty is a Distinguished Professor of Computer Science at UNC Chapel Hill. He was previously a Professor of Electrical Engineering and the Chair of Real-Time Systems at the Technical University of Munich in Germany and has also worked as an Assistant Professor of Computer Science at the National University of Singapore. He holds a PhD in Electrical Engineering from ETH Zurich. He is a Fellow of the IEEE and has received several prizes and awards for his research, including the 2023 Alexander von Humboldt Professorship from Germany. He has extensive collaborations with the industry, and in addition to funding from several governmental agencies, his research has also been supported by grants from General Motors, Intel, Google, BMW, Audi, Siemens and Bosch.
Prof. Sridhar Duggirala is an Assistant Professor in the Department of Computer Science at UNC Chapel Hill. Prior to this, he was an Assistant Professor in the Computer Science and Engineering Department and UTC Institute for Advanced Systems Engineering at the University of Connecticut. He has received his PhD from University of Illinois at Urbana Champaign and has received multiple awards for his research on formal methods, control theory, and hybrid systems.
Prof. Indranil Saha is an Associate Professor and a P. K. Kelkar Faculty Fellow in the Department of Computer Science and Engineering at IIT Kanpur. Prior to joining IIT Kanpur in 2015, he was a postdoctoral researcher affiliated with the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley, and the Department of Computer and Information Science at the University of Pennsylvania. He received his Ph.D. degree in Computer Science from the University of California Los Angeles in 2013. From 2005 to 2008, he was a research scientist at Honeywell, Bangalore. His research interest lies in the application of formal methods and artificial intelligence to embedded and cyber-physical systems and robotics. He was the recipient of a best paper award at the ACM SIGBED International Conference on Embedded Software (EMSOFT) and the ACM SIGBED Frank Anger Memorial Award.
Tutorial Abstract:
Systems that involve a tight integration of models of physical entities (such as their dynamics), algorithms for controlling them, and computational platforms for implementing these algorithms, are referred to as cyber-physical systems (CPS). Autonomous cars and robots are examples of such CPS, where autonomy is implemented using a combination of feedback control and machine learning. While verification of control algorithms, and testing & verification of machine learning algorithms constitute independent research areas, several certification challenges also arise when implementing these algorithms on distributed embedded systems. This is because assumptions made during the design phase of these algorithms—like negligible time needed to compute the control law and zero-delays between the sensors and controllers— do not hold during the implementation phase. Further, there are intricate dependencies between the choice of the machine learning algorithms and the control strategies they feed into. Current approaches towards designing them separately and putting them together in an implementation phase leads to certification challenges with the need for costly testing and debugging. In general, while the principle of separation of concerns has helped tackle design complexity in computer systems, it is increasingly leading to certification problems in the design of autonomous CPS, as assumptions make in designing one component do not hold then it is interfaced with other systems components.
The goal of this tutorial will be to highlight these challenges and discuss emerging design and verification approaches to handle them. It will start by discussing the basics of feedback control systems design, such as state-space formulations, stability, and controller synthesis for linear systems. This will be followed by illustrating how control algorithms interact with their implementation platforms. In particular, we will illustrate model-implementation mismatch because of issues like timing uncertainty during implementation and how to verify controller implementations using reachability analysis techniques. We will also discuss statistical verification techniques and how they can address scalability issues. Finally, we will study certification-driven synthesis of cyber-physical systems.
