Keynotes

Verifying Real-Time Software is Not Reasonable (Today)
Prof. Edward A. Lee (UC Berkeley)

Verification is about demonstrating that a formal system holds certain properties. It is particularly important to verify safety-critical real-time control software, such as aircraft or automotive control systems. Unfortunately, many of the properties that need to be verified for such systems are not actually part of the formal system defined by the software. It therefore makes no sense to verify the software. So what should be verified? It is glib to say that "the system" must be verified, because "the system" is not a formal system. It is a bundle of silicon and wires. Only a model of the system can be verified. What model?

If the semantics of software is extended to include temporal properties, then verifying real-time software becomes possible. In this talk, I will argue that such extensions are practical and effective, but that they require rethinking software abstractions at a rather fundamental level. Moreover, they require reengineering of many performance optimizations that computer architects, compiler designers, and operating system designers have instituted. I will show for some of these that such reengineering yields designs that have competitive performance and verifiable timing.

Speaker Bio
Edward A. Lee is the Robert S. Pepper Distinguished Professor in the Electrical Engineering and Computer Sciences (EECS) department at U.C. Berkeley. His research interests center on design, modeling, and analysis of embedded, real-time computational systems. He is a director of Chess, the Berkeley Center for Hybrid and Embedded Software Systems, and is the director of the Berkeley Ptolemy project. From 2005-2008, he served as chair of the EE Division and then chair of the EECS Department at UC Berkeley. He is co-author of nine books (counting second and third editions) and numerous papers. He has led the development of several influential open-source software packages, notably Ptolemy and its various spinoffs. He received the B.S. degree in Computer Science from Yale University, New Haven, CT, in 1979, the S.M. degree in EECS from the Massachusetts Institute of Technology (MIT), Cambridge, in 1981, and the Ph.D. degree in EECS from the University of California Berkeley, Berkeley, in 1986. From 1979 to 1982 he was a member of technical staff at Bell Telephone Laboratories in Holmdel, New Jersey, in the Advanced Data Communications Laboratory. He is a co-founder of BDTI, Inc., where he is currently a Senior Technical Advisor, and has consulted for a number of other companies. He is a Fellow of the IEEE, was an NSF Presidential Young Investigator, and won the 1997 Frederick Emmons Terman Award for Engineering Education.