Seminars

Computer security aims to ensure only "good" behavior happens in computer systems, despite potential action by malicious adversaries. Consequently, the field has focused primarily on the technology to prohibit "bad things," according to some set of rules, and to a lesser extent on the structure of such rules.  Interestingly, the computer security field has largely ignored the process by which humans produce these sets of rules; not surprisingly, fieldwork and anecdotes report how we keep getting the rules "wrong."

This talk presents some of my lab's research addressing this problem…

The Train Fare Calculation and Adjustment System (TFCAS), developed by the OMRON Corporation, is a large-scale and complex system that helps passengers buy tickets and adjust their train fare on the railways across Japan. In this paper we present the results and experiences gained in a collaborative research project between AIST and OMRON, in which VDM++ has been applied to formalize TFCAS's specifications and validate its consistency as well as reliability properties. An executable VDM++ model can be used to raise the level of the quality of the informal system specification, the…

As the demand on Internet services drastically increases in recent years, the power used by Internet Data Centers (IDCs) has been skyrocketing. How to reduce the power consumptions of IDCs while still providing guaranteed service to end users is a primary concern for IDC operators. In this talk, Professor Liu will first share some challenges and associated opportunities for Internet Data Center power management. He will discuss the power management complexities focusing on micro-level power efficient designs and macro-level resource management, including the hardware, device, software…

The last ten years have seen the coming of age of a range of verification technologies to ensure that programs behave correctly according to their specifications. But checking for errors is only the first step down the road to better more reliable software.  The same technology that can help us discover bugs and verify the correctness of existing software can enable a new class of programming systems that enable more natural and more declarative forms of interaction, and that may ultimately lead to better software that both more reliable and easier to produce.

This talk will…