tasks in a procedural way, says Jackson, developers must first make sure they understand what the system is really about. What are its essential properties? Who are its stakeholders? What level of dependability does it need?

“How can you ever hope to build a dependable system if you don’t know what ‘dependable’ means?” he asks. The task itself is abstract, but Jackson believes that articulating all requirements and assumptions is crucial to tackling it—ideally in a formal, meth-odological way. The most important thing, according to Jackson, is the act of articulation itself. “When you write things down, you often find that you didn’t understand them nearly as well as you thought you did.” And there’s always a temptation to jump to the solution before you’ve fully understood the problem. “That’s not to say that automated tools and techniques like model checking aren’t useful, of course. Tools are an important support, but they’re secondary,” says Jackson.

And the more safety-critical the application, the more rigorous developers must be. “If your computer crashes,

 

Coming Next Month in COMMUNICATIONS

Scaling Massive Multiplayer Online Game Infrastructure

Techniques for Designing Games with a Purpose

Computer Science and Game Theory

The Rise and Fall of CORBA

Evaluating Methodology for the 21st Century

Composable Memory Transactions

Envisioning the Future of Computing Research

CTO Roundtable

Part II of an interview with Donald Knuth

and the latest news about game theory, assistive technologies, and computing and the developing world.

Simpler programs
are easier to verify
with tools like model
checkers.

it’s inconvenient, but it’s not a threat to anyone’s life,” says Holzmann. Among the approaches he and his lab—who work to guarantee the safety of the computer systems that run spacecraft—are currently looking into is the development of simple, yet effective, coding standards. His recommendations may seem somewhat draconian (in safety-critical applications, they forbid the use of goto statements, setjmp or longjmp constructs, and direct or indirect recursion, for example), but they are intended to increase simplicity, prevent common coding mistakes, and force developers to create more logical architectures. Simpler programs are also easier to verify with tools like model checkers. After overcoming their initial reluctance, Holzmann says, developers often find that the restrictions are a worthwhile trade-off for increased safety.

A rigorous focus on simplicity can be costly, of course, especially for complex legacy systems that would be prohibitively expensive to replace but that need, nonetheless, to be updated or further developed. So can taking the time out to formally articulate all requirements and assumptions, or to verify software designs. Yet the cost of fixing an error in the initial stages of development is far less than fixing it at the end—a lesson that Intel, for one, now knows well.

“Computer science is a very young discipline,” explains Joseph Sifakis, research director at CNRS. “We don’t have a theory that can guarantee system reliability, that can tell us how to build systems that are correct by construction. We only have some recipes about how to write good programs and how to design good hardware. We’re learning by a trial-and-error process.”

 

Leah hoffman is a Brooklyn-based freelance writer.

Computer Science
Winning
Strategy

St. Petersburg University of Information Technology, Mechanics and Optics recently won the 32^nd annual ACM International Collegiate Programming Contest (ICPC) World Finals, held in Branff, Canada. It was the university’s second ACM-ICPC world championship in four years.

The annual programming contest started with 6,700 teams from 1,821 universities in 83 countries, competing at 213 sites around the world. Through a series of regional competitions, the field narrowed to 100 teams. At the World Finals, each three-person team had one computer and five hours to solve 11 programming problems.

“The main goal at the World Finals is to solve problems,” says Andrey Stankevich, coach of the St. Petersburg University of Information Technology, Mechanics and Optics team, who was interviewed via email. “If you use your time to solve problems (and not to look for bugs in the problems already solved, but not accepted by the judges) you have time to solve more. So, the way to win the World Finals is to solve problems in such way that you don’t make bugs, and if the problem is accepted, you can immediately start solving another one. This requires cooperation in both thinking about problems and writing code.”

The winning team solved eight problems, followed by second-place Massachusetts Institute of Technology, third-place Izhevsk State Technical University, fourth-place Lviv National University and fifth-place Moscow State University, each of which solved seven problems.

The competition at each ACM-ICPC World Finals appears to be stronger than the previous one, and longtime contest sponsor IBM believes the global contest is good for the I T industry. “The value proposition for IBM is not only about the students who go on to work for IBM, but who go on to work for our clients and our business partners, or who become faculty members,” says IBM director of talent Margaret Ashida. “It’s a win for everyone.”