Alladi Ramakrishnan Hall

Formal Design and Analysis of Cyber-Physical Systems

Ashutosh Trivedi

UPenn, USA

The term {\em cyber-physical systems} (CPS) refers to any network of digital and analog systems whose performance crucially depends on both the continuous dynamics of the analog parts and the real-time switching decisions made by the digital system. Such systems are increasingly playing safety-critical role in modern life, where a fault in their design can be catastrophic. Implantable medical devices are important paradigmatic examples of such safety-critical cyber-physical systems. The growing number of fatalities due to implantable device failures, and an ever increasing list of device recalls by US Food and Drug Administration (FDA) in recent years underscore the challenges in engineering safety-critical CPS. Similar examples can also be cited for CPS from other domains such as avionics, automotive, transportation networks, and energy sector. The central theme underlying my research is to employ rigorous mathematical reasoning to analyze (verification and optimization) and to design (controller synthesis) CPS with guaranteed performance. In this talk I will summarize a few key techniques for formal design and analysis of CPS with emphasis upon my research contributions.

I will also present a recent result on the green scheduling problem where the goal is to co-ordinate switching decisions of various HVAC units so as to minimize the peak energy usage. We pose the green scheduling problem using optimal scheduling problem for constant-rate multi-mode systems (MMS). MMS model hybrid systems that can switch freely among a finite set of modes, and whose dynamics is specified by a finite number of real-valued variables with mode-dependent constant rates. The schedulability problem for such systems is to design a mode-switching policy that maintains the state within a specified safety set. A key result is that the schedulability problem for MMS can be decided in polynomial time. The talk is based on a joint-work with Prof.\ Rajeev Alur and Dr.\ Dominik Wojtczak which has received the best paper award at 15th conference on hybrid systems (HSCC'12) at 2012 Cyber-Physical Systems Week.