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