Seminars

A parallel program must execute correctly even in the presence of unpredictable thread interleavings. This interleaving makes it hard to write correct parallel programs, and also makes it hard to find bugs in incorrect parallel programs. A range of tools have been developed to help debug parallel programs, ranging from atomicity-violation and data-race detectors to model-checkers and theorem provers. One technique that has been successful for debugging sequential programs, but less effective for parallel programs, is running the program using assertion predicates provided by the developer…

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…