don’t know how to verify very complex
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
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
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
Do we have any algorithms that can
operate directly on implementable
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
“if you have
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.