PHOTO: CARNEGIE MELLON UNIVERSITY

IEEE Fellow Jeannette M. Wing is President's Professor of Computer Science and head of the Computer Science Department at Carnegie Mellon University, in Pittsburgh. Her general research interests are in the areas of specification and verification, concurrent and distributed systems, and programming languages.

Prof. Wing is a member of The National Academies' Computer Science and Telecommunications Board. She is a member also of Microsoft's Trustworthy Computing Academic Advisory Board, Intel Research Pittsburgh's Advisory Board, Dartmouth's Institute for Security Technology Studies Advisory Committee, and the Idaho National Laboratory and Homeland Security Strategic Advisory Committee. She was a member of the DARPA Information Science and Technology Board and the National Science Foundation Scientific Advisory Board. She is also a member of the Sloan Research Fellowships Program Committee.

Prof. Wing has worked at Bell Laboratories, the USC Information Sciences Institute, and Xerox Palo Alto Research Center. She spent a sabbatical at MIT in 1992 and another at Microsoft Research from 2002 to 2003. She has consulted for Digital Equipment Corp., the Carnegie Mellon Research Institute, and the Jet Propulsion Laboratory.

Spectrum Online: You work on formal methods. What are formal methods?

Jeannette Wing: A method is formal if it is based on some mathematical system. And people use formal methods to describe systems so that they can check or verify or even predict the behavior properties of the system. And without a formal method you can't really do any kind of analysis, formal analysis, on a system, let alone any kind of prediction of how your system might behave in the real world. I think the best analogy to what a formal method is to a general audience is that what we do is akin to what an architect does in writing blueprints for the design of a building. If you wanted to build a new home, you wouldn't just hire a construction company and say, “Build me a new house.” You'd first hire an architect and say, “Please design a house for me that we can agree on, something I'll like, and then ask the construction company to build according to the blueprint.”

So what formal methods are all about is really the process of writing more formally an architectural description of the system, much like a blueprint for a house. And the practice of software engineering is that people go straight to the construction phase, and they start implementing a system without even knowing what they're supposed to implement. That's why we have a lot of software systems today that are unpredictable and unreliable and insecure. So the point about formal methods is to, in the end, create more reliable software systems, or more reliable systems in general. I think it really shows the state of practice in software engineering: We're not nearly as mature as the architectural construction industry. And we would like to be at least that mature, because the systems that we design are much more malleable, and change, and much more complex than a house.