Tata Institute of Fundamental Research
Formal Design and Analysis of Cyber-Physical Systems
Seminar
Speaker:
Ashutosh Trivedi (University of Pennsylvania
Department of Computer and Information Science
3330 Walnut Street
Philadelphia, PA 19104
United States of America)
Organiser:
John Barretto
Date:
Thursday, 21 Jun 2012, 11:30 to 12:30
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
The term ``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 15h conference on hybrid systems (HSCC'12) at 2012 Cyber-Physical Systems Week.
Bio: Ashutosh Trivedi is a postdoctoral researcher (since 2011) in the computer and information science department at the University of Pennsylvania. He works, broadly, in the area of formal analysis and design of real-time and hybrid systems. After receiving his PhD from the University of Warwick in 2009, he spent 2 years at the University of Oxford as a postdoctoral researcher working as a part of the Large-Scale Complex IT Systems (LSCITS) project. Prior to his PhD, he received a Masters degree in Electrical Engineering (Reliability) from IIT Bombay in 2003, and has worked as research assistant with the CFDVS center at IIT Bombay, the NuSMV development group at IRST, Italy and the formal methods group at University of Tuebingen, Germany.
| Speaker: | Ashutosh Trivedi (University of Pennsylvania Department of Computer and Information Science 3330 Walnut Street Philadelphia, PA 19104 United States of America) |
| Organiser: | John Barretto |
| Date: | Thursday, 21 Jun 2012, 11:30 to 12:30 |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
The term ``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 15h conference on hybrid systems (HSCC'12) at 2012 Cyber-Physical Systems Week.
Bio: Ashutosh Trivedi is a postdoctoral researcher (since 2011) in the computer and information science department at the University of Pennsylvania. He works, broadly, in the area of formal analysis and design of real-time and hybrid systems. After receiving his PhD from the University of Warwick in 2009, he spent 2 years at the University of Oxford as a postdoctoral researcher working as a part of the Large-Scale Complex IT Systems (LSCITS) project. Prior to his PhD, he received a Masters degree in Electrical Engineering (Reliability) from IIT Bombay in 2003, and has worked as research assistant with the CFDVS center at IIT Bombay, the NuSMV development group at IRST, Italy and the formal methods group at University of Tuebingen, Germany.
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 15h conference on hybrid systems (HSCC'12) at 2012 Cyber-Physical Systems Week.
Bio: Ashutosh Trivedi is a postdoctoral researcher (since 2011) in the computer and information science department at the University of Pennsylvania. He works, broadly, in the area of formal analysis and design of real-time and hybrid systems. After receiving his PhD from the University of Warwick in 2009, he spent 2 years at the University of Oxford as a postdoctoral researcher working as a part of the Large-Scale Complex IT Systems (LSCITS) project. Prior to his PhD, he received a Masters degree in Electrical Engineering (Reliability) from IIT Bombay in 2003, and has worked as research assistant with the CFDVS center at IIT Bombay, the NuSMV development group at IRST, Italy and the formal methods group at University of Tuebingen, Germany.