BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/285
DTSTAMP:20230914T125918Z
SUMMARY:Formal Design and Analysis of Cyber-Physical Systems
DESCRIPTION:Speaker: Ashutosh Trivedi (University of Pennsylvania\nDepartme
 nt of Computer and Information Science\n3330 Walnut Street\nPhiladelphia\,
  PA 19104\nUnited States of America)\n\nAbstract: \nThe term ``cyber-physi
 cal systems" (CPS) refers to any network of digital and analog systems who
 se performance crucially depends on both  the continuous dynamics of the 
 analog parts and the real-time switching decisions made by the digital sys
 tem. Such systems are increasingly playing safety-critical role in modern 
 life\, where a fault in their design can be catastrophic. Implantable medi
 cal devices are important paradigmatic examples of such safety-critical cy
 ber-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 i
 n engineering safety-critical CPS. Similar examples can also be cited for 
 CPS from other domains such as avionics\, automotive\, transportation netw
 orks\, and energy sector. The central theme underlying my research is to e
 mploy rigorous mathematical reasoning to analyze (verification and optimiz
 ation) and to design (controller synthesis) CPS with guaranteed performanc
 e. In this talk I will summarize a few key techniques for formal design an
 d analysis of CPS with emphasis upon my research contributions.\n\nI will 
 also present a recent result on the green scheduling problem where the goa
 l is to co-ordinate switching decisions of various HVAC units so as to min
 imize the peak energy usage. We pose the green scheduling problem using op
 timal scheduling problem for constant-rate multi-mode systems (MMS). MMS m
 odel hybrid systems that can switch freely among a finite set of modes\, 
 and whose dynamics is specified by a finite number of real-valued variabl
 es with mode-dependent constant rates. The schedulability problem for suc
 h systems is to design a mode-switching policy that maintains the state w
 ithin a specified safety set. A key result is that  the schedulability pr
 oblem for MMS can be decided in polynomial time. The talk is based on a j
 oint-work with Prof. Rajeev Alur and Dr. Dominik Wojtczak which has receiv
 ed the best paper award at 15h conference on hybrid systems (HSCC'12) at 2
 012 Cyber-Physical Systems Week.\n\nBio: Ashutosh Trivedi is a postdoctora
 l researcher (since 2011) in the computer and information science departme
 nt at the University of Pennsylvania. He works\, broadly\, in the area of 
 formal analysis and design of real-time and hybrid systems. After receivin
 g 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 th
 e Large-Scale Complex IT Systems (LSCITS) project. Prior to his PhD\, he r
 eceived a Masters degree in Electrical Engineering (Reliability) from IIT 
 Bombay in 2003\, and has worked as research assistant with the CFDVS cente
 r at IIT Bombay\,  the NuSMV development group at IRST\, Italy and the fo
 rmal methods group at University of Tuebingen\, Germany.\n
URL:https://www.tcs.tifr.res.in/web/events/285
DTSTART;TZID=Asia/Kolkata:20120621T113000
DTEND;TZID=Asia/Kolkata:20120621T123000
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR