Seminars

Technological advancements in low-power processors, sensors, and radios have boosted the development of single-chip sensor-actuator devices. When distributed over a wide area, networks of these embedded devices can revolutionize a variety of application domains, including environmental monitoring, health care, transportation, defense systems, mobile robotics, manufacturing, smart buildings, and citywide energy optimization.  These cyber-physical systems represent a new class of embedded systems where computation, communication, and control are intimately coupled and introduce new…

I will present some results concerning how we can schedule queries in a sensor network when there is a cost (say, energy) associated with each query. In this setting, how do we make good choices about when to query subject to delay or data staleness limitations? This work provides some guidelines for how to make the tradeoff between delaying the query frequency, which affects energy consumption and data staleness. Starting with the case when all sensors are identical, the talk will also explore the case when there may be two types of sensors: one which is inexpensive to query but may not…

We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of…

The human world is replete with wireless devices. By their broadcast nature, wireless transceivers often cause significant interference to each other if they use the same frequency. This becomes a growing issue as the open 2.4GHz frequency band is being populated by numerous wireless devices including Wi-Fi access points and handhelds, ZigBee sensors, Bluetooth headsets, and cordless phones. In this talk, I will present our recent work on the coexistence of Wi-Fi and ZigBee. Our study of real-life Wi-Fi networks reveals that abundant /white space/ exists in Wi-Fi traffic. We have developed…

The increasing demand for automation in safety-critical applications such as aeronautics, automotive, industrial process control, medical devices and so on, has pressurized the need for scalable formal analysis techniques for ensuring reliable and error-free operation of the systems. A unique feature of these systems is the mixed discrete continuous behaviors they exhibit, which is due to the interaction between a digital computer controlling and a physical entity. From the point of view of computability, presence of the continuous dynamics makes the problem challenging so much so that the…