don’t know how to verify very complex
systems.
emc We’re always playing a catch-
up game; we’re always behind. We’ve
developed more powerful techniques,
but it’s still difficult to keep up with the
advance of technology and the com-
plexity of new systems.
Can we use model checking to check
concurrent programs?
eae Arguably, model checking is a
very natural fit for parallel program-
ming. Typically, we treat parallelism
as a nondeterministic—or, informally,
random—choice, so, in a way a parallel
program is a more complex sequential
program, with many nondeterministic
behaviors. Model checking is very well
suited to describing and reasoning
about the associated coordination and
synchronization properties of parallel
programs.

emc Concurrent programs are much more difficult to debug because it’s difficult for humans to keep track of a lot of things that are happening all at once. Model checking is ideal for that.

JS But if you have programs that interact with the physical environment, time becomes very important. For these systems, verification is much more complicated.

Do we have any algorithms that can
operate directly on implementable
code?

emc To verify the process of translating a design to code, or to verify the code itself, is much more difficult. Some successful model checkers use this approach, however. The Java Pathfinder model checker developed at NASA Ames generates byte code for a Java program and simulates the byte code to find errors.

JS The best available technology is proprietary technology that was developed by U.S. companies. But most of the code-level model checkers are used to verify sequential software. If you want to verify concurrent software, then you need to be very careful.

emc The SLAM model checker developed at Microsoft Research for finding errors in Windows device drivers is probably the most successful software model checker. It is now distributed to people who want to write device drivers for Windows. However, it is hardly a general-purpose software model checker.

“if you have
programs that
interact with
the physical
environment, time
becomes very
important. for
these systems,
verification is
more complicated.”

eae In hardware verification, Verilog and VHDL are widely used design description languages. Many industrial model checkers typically accept designs described in these languages.

Is model checking something cur-
rently taught to undergraduates?

JS Formal verification is definitely
taught in Europe. Europe has tradition-
ally had a stronger community in for-
mal methods, and I’d like to say it has
also traditionally had a stronger com-
munity in semantics and languages.
emc Yes, there’s always been more in-
terest in verification in Europe than in
the U.S. Most of the major universities
here—CMU, Stanford, UC Berkeley, U.
Texas, and so on—do offer courses in
model checking at both undergradu-
ate and graduate levels, but it hasn’t fil-
tered down to schools where no one is
doing research in the topic. Part of that
has to do with the availability of appro-
priate textbooks; good books are just
beginning to come out.

eae Formal methods are being taught with some frequency [in the U.S.], but they are not broadly incorporated into the core undergraduate curriculum as required courses to the extent that operating systems and data structures are. It is probably more prevalent at the graduate level. But the distinction between undergraduate and graduate is not clear-cut. At many schools advanced undergrad and beginning grad overlap.

What’s in store for model checking
and formal verification?

emc I intend to continue looking at ways of making model checking more powerful. The state explosion phenomenon is still a difficult problem. I have worked on it for 27 years and probably will continue to do so. Another thing I want to do is focus on embedded software systems in automotive and avionics applications. These programs are often safety-critical. For example, in a few years, cars will be “drive-by-wire”; there will be no mechanical linkage between the steering wheel and the tires. The software will definitely need to be verified. Fortunately, embedded software is usually somewhat simpler in structure, without complex pointers; I think it may be more amenable to model checking techniques than general software.

JS Personally, I believe we should look into techniques that allow some sort of compositional reasoning, where we infer global properties from local properties of the system, because of the inherent limitations of techniques based on the analysis of a global model. I’m working on this, as well as on theories of how to build systems out of components, component-based systems.

eae Model checking has caused a sea change in the way we think about establishing program correctness, from proof-theoretic (deductive proof) to model-theoretic (graph search). I think we will continue to make more or less steady progress, but the pace of development of hardware and software is going to accelerate. Whether we ever catch up I don’t know. Systems that are being designed are getting bigger and messier. The seat-of-the-pants approach will no longer work. We’ll have to get better at doing things modularly, and we’ll have to have better abstractions.

 

Leah hoffman writes about science and technology from Brooklyn, NY.