Kaushik Mallik, Researcher, the Institute of Science and Technology Austria
Cyber-physical systems (CPS) are now ubiquitous among automated technologies, in which physical dynamical systems are operated via software-based controllers. Since a majority of CPS applications are safety-critical, certifying correctness of their controllers is an important research problem. A promising approach is to use formal methods, which enables us to design CPS controllers with rigorous correctness guarantees with respect to given specifications. Unfortunately, the formal methods approaches still face practical bottlenecks (like scalability and expressiveness) in the real-world applications. In this talk, I will present my works and my vision towards verified controller design for real-world CPS systems. In particular, I will present a collection of new design principles that are computationally superior and can support richer classes of system models than the state-of-the-art. Additionally, I will share my vision for controller design principles that can put safeguards against anomalous events that may occur during deployment—a realistic scenario that lacks systematic support in the current literature.