Seminars

High-fidelity models of airport and airspace capacity enable researchers to study modernization strategies that optimize capacity yet require volumes of detailed aircraft movement data. These datasets exist in the public and private realms but are highly challenging and cumbersome to collect in large quantities. In this talk I will present my real-time data scraping and mathematical modeling methodology to collect and augment real-time trajectory data. Using this data, I present an airport planning study and a study of airspace resiliency. I study the change in terminal area flows due to…

Developing correct parallel and distributed software is a daunting task. The parallelism causes the state-spaced explosion problem: the number of states in the system grows exponentially with the number of parallel components. One of the ways to verify that such a system satisfies its requirements is model checking.

In this talk, I will describe the application of model checking to two real-world systems, and describe the errors that were uncovered using this approach.

The first system is the session setup protocol that is part of the IEEE 11073-20601:2008 standard for…

For economic reasons, the design and fabrication of semiconductor ICs is increasingly outsourced. This comes at the expense of trust. An untrusted entity, for instance a malicious designer or semiconductor foundry could pirate the design, or worse, maliciously modify it to leak secret information from the chip or sabotage its functionality. In addition, several companies now provide IC reverse engineering services that can reconstruct a manufactured chip's internal design details, thus compromising the designer's IP. Reverse engineering attack's on embedded devices and smart-cards have…

Energy-efficiency is a critical concern in continuously-running mobile applications, such as those for health and context monitoring. An attractive approach to saving energy in such applications is to defer the execution of delay-tolerant op- erations until a time when they would consume less energy. However, introducing delays to save power may have a detri- mental impact on the user experience. To address this prob- lem, we present Tempus, a new approach to managing the trade-off between energy savings and delay. Tempus saves power by enabling programmers to annotate power-hungry…

The realization of complex cyber-physical systems is creating design and verification challenges that will soon become insurmountable with today’s engineering practices. While model-based design tools are already facilitating several design tasks, harnessing the complexity of the Internet-of-Things scenario is only deemed possible within a unifying methodology. This methodology should help interconnect different tools, possibly operating on different system representations, to enable scalable design space exploration and early detection of requirement inconsistencies.

In this talk…