EDMUND M. ClARkE, E. Allen Emerson, and Joseph Sifakis were honored for their role in developing Model-Checking into a highly effective verification technology, widely adopted in the hardware and software industries.
Let’s talk about the history of formal software verification. e. aLLen emeRSon By the late 1960s, we recognized that a program should be viewed as a mathemat ical object. It has a syntax and semantics and formally defined behavior engendered by that syntax and semantics. The idea was to give a mathematical proof that a program met a certain correctness specification. So one would have some axioms characterizing the way the program worked for such-and-such an instruction and some inference rules, and one would construct a formal proof of the system, like philosophers do sometimes. But it never really seemed to scale up to large programs. You ended up with something like 15-page papers proving that a half-page program was correct. It was a great idea but didn’t seem to pan out in practice. What about the history of model checking? eDmunD m. cLaRKe The birth of model checking was quite painful at times. Like most research on the boundary between theory and practice, theoreticians thought the idea was trivial, and system builders thought it was too theoretical. Researchers in formal methods were
even less receptive. Research in the for-
mal-methods community in the 1980s
usually consisted of designing and
verifying tricky programs with fewer
than 50 lines using only pen and paper.
If anyone asked how such a program
worked in practice on a real computer,
it would have been interpreted as an in-
sult or perhaps simply as irrelevant.
eae The idea behind model check-
ing was to avoid having humans con-
struct proofs. It turns out that many
important programs, such as operating
systems, have ongoing behavior and
ideally run forever; they don’t just start
and stop. In 1977, Amir Pnueli suggest-
ed that temporal logic could be a good
way to describe and reason about these
programs. Now, if a program can be
specified in temporal logic, then it can
be realized as a finite state program—
a program with just a finite number
of different configurations. This sug-
gested the idea of model checking—to
check whether a finite state graph is a
model of a temporal logic specifica-
tion. Then one can develop efficient
algorithms to check whether the tem-
poral-logic specification is true of the
state graph by searching through the
state graph for certain patterns.
emc Yes, Allen and I noticed that many concurrent programs had what we called “finite state synchronization skeletons.” (Joseph Sifakis and J.P. Queille made the same observation, independently.) For example, the part of a mutual-exclusion program that handles synchronization does not depend
References:
Archives