Tuesday Apr. 20, 2004, 4:15-5:45 pm, 3400 Boelter Hall

Model-Driven Software Verification

Gerard J. Holzmann
Jet Propulsion Laboratory

The current focus in logic model checking in software verification targets
the elimination of the need for hand-constructed models.
In the <http://cm.bell-labs.com/cm/cs/what/feaver/>FeaVer project we used
automated model extraction from C code to address this problem. In this
talk I will describe a new, and possibly simpler, method, that allows us to
link a logic model checker (e.g., <http://spinroot.com>Spin) directly to
unmodified application level code. We now write a non-deterministic
test-harness as a Spin model, to drive the application through all its
relevant states, while the model checker verifies its logic properties.
Notably, the model checker can use powerful data abstraction techniques in
this verification process, while the application uses only concrete data
representations.  He will give some examples of the application of this
method to the verification of critical pieces of flight software for a
recent JPL mission.

Dr. Gerard J. Holzmann is best known as the designer of the Spin model
checker, which was recognized in 2001 with the ACM Software Systems Award.
Formerly a Director of the Computing Principles Research group at Bell Labs
in Murray Hill, NJ, Holzmann joined NASA's Jet Propulsion Laboratory in
2003 to start a new Laboratory for Reliable Software. Holzmann holds 7
patents, one of which received the 2003 Thomas Alva Edison Award in
Information Technology from the Research and Development Council of New
Jersey. He has written several books, including "The Spin Model Checker"
(Addison-Wesley, 2004), "The Early History of Data Networks" (IEEE CS
Press, 1995), and "Beyond Photography: The Digital Darkroom" (Prentice
Hall, 1987).

Host: Rupak Majumdar